default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDFM 2021: Virtual Event
- Marieke Huisman
, Corina S. Pasareanu, Naijun Zhan:
Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings. Lecture Notes in Computer Science 13047, Springer 2021, ISBN 978-3-030-90869-0
Invited Presentations
- Paula Herber, Timm Liebrenz, Julius Adelt:
Combining Forces: How to Formally Verify Informally Defined Embedded Systems. 3-22 - Mingsheng Ying:
Model Checking for Verification of Quantum Circuits. 23-39
Interactive Theorem Proving
- Matt Griffin, Brijesh Dongol:
Verifying Secure Speculation in Isabelle/HOL. 43-60 - Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, Philippa Gardner:
Two Mechanisations of WebAssembly 1.0. 61-79
Neural Networks and Active Learning
- Bing Sun, Jun Sun, Ting Dai, Lijun Zhang:
Probabilistic Verification of Neural Networks Against Group Fairness. 83-102 - Joseph Scott, Trishal Sudula, Hammad Rehman, Federico Mora, Vijay Ganesh:
BanditFuzz: Fuzzing SMT Solvers with Multi-agent Reinforcement Learning. 103-121 - Alexei Kopylov, Stefan Mitsch, Aleksey Nogin, Michael A. Warren:
Formally Verified Safety Net for Waypoint Navigation Neural Network Controllers. 122-141 - Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak:
Model-Free Reinforcement Learning for Lexicographic Omega-Regular Objectives. 142-159
Logics and Theory
- Gal Amram, Shahar Maoz, Or Pistiner, Jan Oliver Ringert:
Efficient Algorithms for Omega-Regular Energy Games. 163-181 - Shankara Narayanan Krishna, Khushraj Madnani, Manuel Mazo Jr., Paritosh K. Pandya:
Generalizing Non-punctuality for Timed Temporal Logic with Freeze Quantifiers. 182-199 - Matias Scharager, Katherine Cordwell, Stefan Mitsch, André Platzer:
Verified Quadratic Virtual Substitution for Real Arithmetic. 200-217 - Rim Saddem-Yagoubi, Pascal Poizat, Sara Houhou:
Business Processes Meet Spatial Concerns: The sBPMN Verification Framework. 218-234
Program Verification I
- Daniel Wright, Mark Batty, Brijesh Dongol:
Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies. 237-254 - Jinting Bian, Hans-Dieter A. Hiep, Frank S. de Boer, Stijn de Gouw:
Integrating ADTs in KeY and Their Application to History-Based Reasoning. 255-272 - Alexandra Bugariu, Arshavir Ter-Gabrielyan, Peter Müller:
Identifying Overly Restrictive Matching Patterns in SMT-Based Program Verifiers. 273-291 - Nicholas Coughlin, Kirsten Winter, Graeme Smith:
Rely/Guarantee Reasoning for Multicopy Atomic Weak Memory Models. 292-310
Hybrid Systems
- Sota Sato, Atsuyoshi Saimen, Masaki Waga, Kenji Takao, Ichiro Hasuo:
Hybrid System Falsification for Multiple-Constraint Parameter Synthesis: A Gas Turbine Case Study. 313-329 - Zhenya Zhang, Paolo Arcaini:
Gaussian Process-Based Confidence Estimation for Hybrid System Falsification. 330-348 - Julius Adelt, Timm Liebrenz, Paula Herber:
Formal Verification of Intelligent Hybrid Systems that are Modeled with Simulink and the Reinforcement Learning Toolbox. 349-366 - Simon Foster, Jonathan Julián Huerta y Munive, Mario Gleirscher, Georg Struth:
Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs. 367-386
Program Verification II
- Federico Mora, Murphy Berzish, Mitja Kulczynski, Dirk Nowotka, Vijay Ganesh:
Z3str4: A Multi-armed String Solver. 389-406 - Felix A. Wolf, Malte Schwerhoff, Peter Müller:
Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA. 407-426 - Adel Djoudi, Martin Hána, Nikolai Kosmatov:
Formal Verification of a JavaCard Virtual Machine with Frama-C. 427-444 - Franck Cassez:
Verification of the Incremental Merkle Tree Algorithm with Dafny. 445-462
Automata
- Yong Li, Yih-Kuen Tsay, Andrea Turrini, Moshe Y. Vardi, Lijun Zhang:
Congruence Relations for Büchi Automata. 465-482 - Maurice H. ter Beek, Guillermina Cledou, Rolf Hennicker, José Proença:
Featured Team Automata. 483-502 - Anastasia Mavridou, Andreas Katis, Dimitra Giannakopoulou, David Kooi, Thomas Pressburger, Michael W. Whalen:
From Partial to Global Assume-Guarantee Contracts: Compositional Realizability Analysis in FRET. 503-523 - Andrea Pferscher, Bernhard K. Aichernig:
Fingerprinting Bluetooth Low Energy Devices via Active Automata Learning. 524-542
Analysis of Complex Systems
- Weijiang Hong, Zhenbang Chen, Yide Du, Ji Wang:
Trace Abstraction-Based Verification for Uninterpreted Programs. 545-562 - Felipe Gorostiaga, César Sánchez:
HStriver: A Very Functional Extensible Tool for the Runtime Verification of Real-Time Event Streams. 563-580 - Cui Su, Jun Pang:
Cabean 2.0: Efficient and Efficacious Control of Asynchronous Boolean Networks. 581-598 - Ionut Tutu, Claudia Elena Chirita, José Luiz Fiadeiro:
Dynamic Reconfiguration via Typed Modalities. 599-615
Probabilities
- Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný, Jiri Zárevúcky, Dorde Zikelic:
On Lexicographic Proof Rules for Probabilistic Termination. 619-639 - Frantisek Blahoudek, Murat Cubuktepe, Petr Novotný, Melkior Ornik, Pranay Thangeda, Ufuk Topcu:
Fuel in Markov Decision Processes (FiMDP): A Practical Approach to Consumption. 640-656 - Oyendrila Dobe, Erika Ábrahám, Ezio Bartocci, Borzoo Bonakdarpour:
HyperProb: A Model Checker for Probabilistic Hyperproperties. 657-666 - Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovács:
The Probabilistic Termination Tool Amber. 667-675 - Rong Gu, Cristina Seceleanu, Eduard Enoiu, Kristina Lundqvist:
Model Checking Collision Avoidance of Nonlinear Autonomous Vehicles. 676-694
Industry Track Invited Papers
- Carl-Johan H. Seger:
Formal Verification of Complex Data Paths: An Industrial Experience. 697-716 - Grant Olney Passmore:
Some Lessons Learned in the Industrialization of Formal Methods for Financial Algorithms. 717-721
Industry Track
- Tino Teige, Andreas Eggers, Karsten Scheibler, Matthias Stasch, Udo Brockmeyer, Hans Jürgen Holberg, Tom Bienmüller:
Two Decades of Formal Methods in Industrial Products at BTC Embedded Systems. 725-729 - Panagiotis Kouvaros, Trent Kyono, Francesco Leofante, Alessio Lomuscio, Dragos D. Margineantu, Denis Osipychev, Yang Zheng:
Formal Analysis of Neural Network-Based Systems in the Aircraft Domain. 730-740 - Song Gao, Bohua Zhan, Depeng Liu, Xuechao Sun, Yanan Zhi, David N. Jansen, Lijun Zhang:
Formal Verification of Consensus in the Taurus Distributed Database. 741-751 - Jiawan Wang, Lei Bu, Shaopeng Xing, Yuming Wu, Xuandong Li:
Combined Online Checking and Control Synthesis: A Study on a Vehicle Platoon Testbed. 752-762 - Yousaf Rahman, Md Tawhid Bin Waez, Yuming Niu:
Formally Guaranteed Tight Dynamic Future Occupancy of Autonomous Vehicles. 763-775 - César Augusto Ribeiro dos Santos, Tom Schrijvers, Amr Hany Saleh, Mike Nicolai:
Divide et Impera: Efficient Synthesis of Cyber-Physical System Architectures from Formal Contracts. 776-787 - Wenjing Xu, Yongwang Zhao, Chengtao Cao, Jean Raphael Ngnie Sighom, Lei Wang, Zhe Jiang, Shihong Zou:
Apply Formal Methods in Certifying the SyberX High-Assurance Kernel. 788-798
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2026-01-16 23:39 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
