Proceedings of Formal Methods in Computer-Aided Design, FMCAD 2022




Formal Methods in Computer Aided Design

Journal Title

Journal ISSN

Volume Title


TU Wien Academic Press



The Conference on Formal Methods in Computer-Aided Design (FMCAD) is an annual conference on the theory and applications of formal methods in hardware and system verification. FMCAD provides a leading forum to researchers in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for reasoning formally about computing systems. FMCAD covers formal aspects of computer-aided system design including verification, specification, synthesis, and testing.
Table of Contents: Invited Talks -- The seL4 Verification Journey: How Have the Challenges and Opportunities Evolved / by June Andronick (p. 1) -- Why Do Things Go Wrong (or Right)? Applications of Causal Reasoning to Verification / by Hana Chockler (p. 2) -- Tutorials -- On Applying Model Checking in Formal Verification / by Håkan Hjort (p. 3) -- Verification of Distributed Protocols: Decidable Modeling and Invariant Inference / by Oded Padon (p. 4) -- Student Forum -- The FMCAD 2022 Student Forum / by Matthias Preiner (p. 5) -- Verification in Machine Learning -- Proving Robustness of KNN Against Adversarial Data Poisoning / by Yannan Li, Jingbo Wang and Chao Wang (p. 7) -- On Optimizing Back-Substitution Methods for Neural Network Verification / by Tom Zelazny, Haoze Wu, Clark Barrett and Guy Katz (p. 17) -- Verification-Aided Deep Ensemble Selection ./ by Guy Amir, Tom Zelazny, Guy Katz and Michael Schapira (p. 27) -- Neural Network Verification with Proof Production / by Omri Isac, Clark Barrett, Min Zhang and Guy Katz (p. 38) -- Proofs -- TBUDDY: A Proof-Generating BDD Package / by Randal Bryant (p. 49) -- Stratified Certification for k-Induction / by Emily Yu, Nils Frolyeks, Armin Biere and Keijo Heljanko (p. 59) -- Reconstructing Fine-Grained Proofs of Complex Rewrites Using a Domain-Specific Language / by Andres Noetzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Cesare Tinelli and Clark Barrett (p. 65) -- Small Proofs from Congruence Closure / by Oliver Flatt, Samuel Coward, Max Willsey, Zachary Tatlock and Pavel Panchekha (p. 75) -- Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers / by Abhishek Nair, Saranyu Chattopadhyay, Haoze Wu, Alex Ozdemir and Clark Barrett (p. 84) -- Hardware and RTL -- Reconciling Verified-Circuit Development and Verilog Development / by Andreas Lööw (p. 89) -- Timed Causal Fanin Analysis for Symbolic Circuit Simulation / by Roope Kaivola and Neta Bar Kama (p. 99) -- Divider Verification Using Symbolic Computer Algebra and Delayed Don’t Care Optimization / by Alexander Konrad, Christoph Scholl, Alireza Mahzoon, Daniel Große and Rolf Drechsler (p. 108) -- Formally Verified Isolation of DMA / by Jonas Haglund and Roberto Guanciale (p. 118) -- Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution / by Karl Palmskog, Xiaomo Yao, Ning Dong, Roberto Guanciale and Mads Dam (p. 129) -- Synthesizing Instruction Selection Rewrite Rules from RTL using SMT / by Ross Daly, Caleb Donovick, Jack Melchert, Raj Setaluri, Nestan Tsiskaridze, Priyanka Raina, Clark Barrett and Pat Hanrahan (p. 139) -- Error Correction Code Algorithm and Implementation Verification using Symbolic Representations / by Aarti Gupta, Roope Kaivola, Mihir Parang Mehta and Vaibhav Singh (p. 151) -- SAT and SMT -- First-Order Subsumption via SAT Solving / by Jakob Rath, Armin Biere and Laura Kovacs (p. 160) -- BaxMC: a CEGAR approach to MAX#SAT / by Thomas Vigouroux, Cristian Ene, David Monniaux, Laurent Mounier and Marie-Laure Potet (p. 170) -- Compact Symmetry Breaking for Tournaments / by Evan Lohn, Chris Lambert and Marijn Heule (p. 179) -- Enumerative Data Types with Constraints / by Andrew T Walter, David Greve and Panagiotis Manolios (p. 189) -- Reducing NEXP-complete problems to DQBF / by Fa-Hsun Chen, Shen-Chang Huang, Yu-Cheng Lu and Tony Tan (p. 199) -- INC: A Scalable Incremental Weighted Sampler / by Suwei Yang, Victor Liang and Kuldeep S. Meel (p. 205) -- Bounded Model Checking for LLVM / by Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao and Arie Gurfinkel (p. 214) -- Parameterized Systems and Quantified Reasoning -- Automatic Repair and Deadlock Detection for Parameterized Systems / by Swen Jacobs, Mouhammad Sakr and Marcus Völp (p. 225) -- Synthesizing Locally Symmetric Parameterized Protocols from Temporal Specifications / by Ruoxi Zhang, Richard Trefler and Kedar Namjoshi (p. 235) -- Synthesizing Self-Stabilizing Parameterized Protocols with Unbounded Variables / by Ali Ebnenasir (p. 245) -- The Rapid Software Verification Framework / by Pamina Georgiou, Bernhard Gleiss, Ahmed Bhayat, Michael Rawson, Laura Kovacs and Giles Reger (p. 255) -- Distributed Systems -- ACORN: Network Control Plane Abstraction using Route Nondeterminism / by Divya Raghunathan, Ryan Beckett, Aarti Gupta and David Walker (p. 261) -- Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+ / by William Schultz, Ian Dardik and Stavros Tripakis (p. 273) -- Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens / by Bengt Jonsson, Magnus Lång and Kostis Sagonas (p. 284) -- Synthesis -- Synthesizing Transducers from Complex Specifications / by Anvay Grover, Rüdiger Ehlers and Loris D’Antoni (p. 294) -- Synthesis of Semantic Actions in Attribute Grammars / by Pankaj Kumar Kalita, Miriyala Jeevan Kumar and Subhajit Roy (p. 304) -- Reactive Synthesis Modulo Theories using Abstraction Refinement / by Benedikt Maderbacher and Roderick Bloem (p. 315) -- Learning Deterministic Finite Automata Decompositions from Examples and Demonstrations / by Niklas Lauffer, Beyazit Yalcinkaya, Marcell Vazquez-Chanlatte, Ameesh Shah and Sanjit A. Seshia (p. 325) -- Reachability and Safety Verification -- Automated Conversion of Axiomatic to Operational Models: Theoretical and Practical Results / by Adwait Godbole, Yatin A. Manerkar and Sanjit A. Seshia (p. 331) -- Formally Verified Quite OK Image Format / by Mario Bucev and Viktor Kunčak (p. 343) -- Split Transition Power Abstraction for Unbounded Safety / by Martin Blicha, Grigory Fedyukovich, Antti Hyvärinen and Natasha Sharygina (p. 349) -- Automating Geometric Proofs of Collision Avoidance with Active Corners / by Nishant Kheterpal, Elanor Tang and Jean-Baptiste Jeannin (p. 359) -- Differential Testing of Pushdown Reachability with a Formally Verified Oracle / by Anders Schlichtkrull, Morten Konggaard Schou, Jiri Srba and Dmitriy Traytel (p. 369) -- TriCera: Verifying C Programs Using the Theory of Heaps / by Zafer Esen and Philipp Ruemmer (p. 380)

LCSH Subject Headings


Griggio, A., & Rungta, N. (Eds.). (2022). Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (Vol. 3). TU Wien Academic Press.