{"id":1152,"date":"2021-08-23T14:16:25","date_gmt":"2021-08-23T06:16:25","guid":{"rendered":"http:\/\/lcs.ios.ac.cn\/fm2021\/?page_id=1152"},"modified":"2021-08-23T14:39:37","modified_gmt":"2021-08-23T06:39:37","slug":"accepted-papers","status":"publish","type":"page","link":"http:\/\/lcs.ios.ac.cn\/fm2021\/accepted-papers\/","title":{"rendered":"FM Accepted Papers"},"content":{"rendered":"

Rong Gu<\/span><\/a>, Cristina Seceleanu, Eduard Enoiu and Kristina Lundqvist. Model Checking Collision Avoidance of Nonlinear Autonomous Vehicle Models<\/em><\/p>\n

Oyendrila Dobe, Erika Abraham<\/a><\/span>, Ezio Bartocci<\/a><\/span> and Borzoo Bonakdarpour<\/a><\/span>. HyperProb: A Model Checker for Probabilistic Hyperproperties<\/em><\/p>\n

Bing Sun, Jun Sun, Ting Dai and Lijun Zhang. Probabilistic Verification of Neural Networks Against Group Fairness<\/em><\/p>\n

Gal Amram, Shahar Maoz<\/a><\/span>, Or Pistiner and Jan Oliver Ringert<\/a><\/span>. Efficient Algorithms for \u03c9-Regular Energy Games<\/em><\/p>\n

Alexei Kopylov<\/span><\/a>, Stefan Mitsch, Aleksey Nogin<\/a><\/span> and Michael Warren<\/a><\/span>. Formally Verified Safety Net for Waypoint Navigation Neural Network Controllers<\/em><\/p>\n

Matt Griffin and Brijesh Dongol<\/a><\/span>. Verifying Secure Speculation in Isabelle\/HOL<\/em><\/p>\n

Felix A. Wolf, Malte Schwerhoff and Peter M\u00fcller<\/a><\/span>. Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA<\/em><\/p>\n

Sota Sato, Atsuyoshi Saimen, Masaki Waga<\/a><\/span>, Kenji Takao and Ichiro Hasuo<\/a><\/span>. Hybrid System Falsification for Multiple-Constraint Parameter Synthesis: a Gas Turbine Case Study<\/em><\/p>\n

Rim Saddem-Yagoubi, Pascal Poizat<\/a><\/span> and Sara Houhou. Business Processes Meet Spatial Concerns: the sBPMN Verification Framework<\/em><\/p>\n

Mark Batty<\/span><\/a>, Brijesh Dongol<\/span><\/a> and Daniel Wright. Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies<\/em><\/p>\n

Julius Adelt<\/span><\/a>, Timm Liebrenz<\/a> <\/span>and Paula Herber<\/a><\/span>. Formal Verification of Intelligent Hybrid Systems that are modeled with Simulink and the Reinforcement Learning Toolbox<\/em><\/p>\n

Marcel Moosbrugger<\/span><\/a>, Ezio Bartocci, Joost-Pieter Katoen and Laura Kov\u00e1cs. The Probabilistic Termination Tool Amber<\/em><\/p>\n

Adel Djoudi, Martin Hana and Nikolai Kosmatov<\/a><\/span>. Formal verification of a JavaCard virtual machine with Frama-C<\/em><\/p>\n

Felipe Gorostiaga and Cesar Sanchez<\/a><\/span>. HStriver: a Very Functional Extensible Tool for the Runtime Verification of Real-Time Event Streams<\/em><\/p>\n

Matias Scharager, Katherine Cordwell, Stefan Mitsch and Andr\u00e9 Platzer<\/a><\/span>. Verified Quadratic Virtual Substitution for Real Arithmetic<\/em><\/p>\n

Nicholas Coughlin, Kirsten Winter and Graeme Smith<\/a><\/span>. Rely\/guarantee reasoning for multicopy atomic weak memory models<\/em><\/p>\n

Franck Cassez<\/a><\/span>. Verification of the Incremental Merkle Tree Algorithm with Dafny<\/em><\/p>\n

Weijiang Hong, Zhenbang Chen<\/a><\/span>, Yide Du and Ji Wang. Trace Abstraction-based Verification for Uninterpreted Programs<\/em><\/p>\n

Cui Su and Jun Pang<\/a><\/span>. CABEAN 2.0: Efficient and Efficacious Control of Asynchronous Boolean Networks<\/em><\/p>\n

Jinting Bian, Hans-Dieter Hiep<\/a><\/span>, Frank De Boer and Stijn De Gouw<\/a><\/span>. Integrating ADTs in KeY and their Application to History-based Reasoning<\/em><\/p>\n

Yong Li<\/a><\/span>, Yih-Kuen Tsay<\/a><\/span>, Andrea Turrini<\/a><\/span>, Moshe Vardi<\/span><\/a> and Lijun Zhang. Congruence Relations for B\u00fcchi Automata<\/em><\/p>\n

Krishnendu Chatterjee<\/span><\/a>, Ehsan Kafshdar Goharshady, Petr Novotn\u00fd<\/a><\/span>, Ji\u0159\u00ed Z\u00e1rev\u00facky and Djordje Zikelic. On Lexicographic Proof Rules for Probabilistic Termination<\/em><\/p>\n

Franti\u0161ek Blahoudek, Murat Cubuktepe<\/a><\/span>, Petr Novotn\u00fd<\/a><\/span>, Melkior Ornik<\/span><\/a>, Pranay Thangeda<\/span><\/a> and Ufuk Topcu. Fuel in Markov Decision Processes (FiMDP): A Practical Approach to Consumption<\/em><\/p>\n

Ionut Tutu, Claudia Chirita and Jos\u00e9 Luiz Fiadeiro<\/a><\/span>. Dynamic Reconfiguration via Typed Modalities<\/em><\/p>\n

Simon Foster, Mario Gleirscher, Jonathan Huerta Y Munive and Georg Struth<\/span><\/a>. Hybrid Systems Verification with Isabelle\/HOL: Simpler Syntax, Better Models, Faster Proofs<\/em><\/p>\n

Andrea Pferscher and Bernhard K. Aichernig<\/span><\/a>. Fingerprinting Bluetooth Low Energy Devices via Active Automata Learning<\/em><\/p>\n

Alexandra Bugariu, Arshavir Ter-Gabrielyan and Peter M\u00fcller. Identifying Overly Restrictive Matching Patterns in SMT-based Program Verifiers<\/em><\/p>\n

Maurice ter Beek<\/span><\/a>, Guillermina Cledou<\/a><\/span>, Rolf Hennicker<\/a> <\/span>and Jos\u00e9 Proen\u00e7a<\/a><\/span>. Featured Team Automata<\/em><\/p>\n

Ernst Moritz Hahn, Mateo Perez, Sven Schewe<\/span><\/a>, Fabio Somenzi<\/a><\/span>, Ashutosh Trivedi<\/a> <\/span>and Dominik Wojtczak<\/a><\/span>. Model-Free Reinforcement Learning for Lexicographic Omega-Regular Objectives<\/em><\/p>\n

Federico Mora, Murphy Berzish, Mitja Kulczynski, Dirk Nowotka<\/a> <\/span>and Vijay Ganesh<\/span><\/a>. Z3str4: A Multi-armed String Solver<\/em><\/p>\n

Anastasia Mavridou<\/a><\/span>, Andreas Katis, Dimitra Giannakopoulou<\/span><\/a>, David Kooi, Thomas Pressburger<\/a> <\/span>and Michael W. Whalen. From Partial to Global Assume-Guarantee Contracts: Compositional Realizability Analysis in FRET<\/em><\/p>\n

Joseph Scott, Hammad Rehman, Trishal Sudula, Federico Mora and Vijay Ganesh<\/a><\/span>. BanditFuzz: Fuzzing SMT Solvers with Multi-Agent Reinforcement Learning<\/em><\/p>\n

Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin and Philippa Gardner. Two mechanisations of WebAssembly 1.0<\/em><\/p>\n

Krishna S<\/span><\/a>, Khushraj Madnani<\/a><\/span>, Manuel Mazo Jr<\/span>.<\/a> and Paritosh Pandya<\/a><\/span>. Generalizing Non-Punctuality for Timed Temporal Logic with Freeze Quantifiers<\/em><\/p>\n

Zhenya Zhang and Paolo Arcaini<\/span><\/a>. Gaussian Process-Based Confidence Estimation for Hybrid System Falsification<\/em><\/p>\n<\/div><\/div><\/div>