PROCEEDINGS OF THE 22ND CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN – FMCAD 2022

Contents

Invited Talks
The seL4 Verification Journey: How Have the Challenges and Opportunities Evolved
June Andronick

Why Do Things Go Wrong (or Right)? Applications of Causal Reasoning to Verification
Hana Chockler

Tutorials
On Applying Model Checking in Formal Verification
Håkan Hjort

Verification of Distributed Protocols: Decidable Modeling and Invariant Inference
Oded Padon

Student Forum
The FMCAD 2022 Student Forum
Matthias Preiner

Verification in Machine Learning
Proving Robustness of KNN Against Adversarial Data Poisoning
Yannan Li, Jingbo Wang and Chao Wang

On Optimizing Back-Substitution Methods for Neural Network Verification
Tom Zelazny, Haoze Wu, Clark Barrett and Guy Katz

Verification-Aided Deep Ensemble Selection
Guy Amir, Tom Zelazny, Guy Katz and Michael Schapira

Neural Network Verification with Proof Production
Omri Isac, Clark Barrett, Min Zhang and Guy Katz 

Proofs
TBUDDY: A Proof-Generating BDD Package
Randal Bryant

Stratified Certification for k-Induction
Emily Yu, Nils Frolyeks, Armin Biere and Keijo Heljanko

Reconstructing Fine-Grained Proofs of Complex Rewrites Using a Domain-Specific Language
Andres Noetzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Cesare Tinelli and Clark Barrett

Small Proofs from Congruence Closure
Oliver Flatt, Samuel Coward, Max Willsey, Zachary Tatlock and Pavel Panchekha

Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers
Abhishek Nair, Saranyu Chattopadhyay, Haoze Wu, Alex Ozdemir and Clark Barrett

Hardware and RTL
Reconciling Verified-Circuit Development and Verilog Development
Andreas Lööw

Timed Causal Fanin Analysis for Symbolic Circuit Simulation
Roope Kaivola and Neta Bar Kama

Divider Verification Using Symbolic Computer Algebra and Delayed Don’t Care Optimization
Alexander Konrad, Christoph Scholl, Alireza Mahzoon, Daniel Große and Rolf Drechsler

Formally Verified Isolation of DMA
Jonas Haglund and Roberto Guanciale

Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution
Karl Palmskog, Xiaomo Yao, Ning Dong, Roberto Guanciale and Mads Dam

Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
Ross Daly, Caleb Donovick, Jack Melchert, Raj Setaluri, Nestan Tsiskaridze, Priyanka Raina, Clark Barrett and Pat Hanrahan

Error Correction Code Algorithm and Implementation Verification using Symbolic Representations
Aarti Gupta, Roope Kaivola, Mihir Parang Mehta and Vaibhav Singh

SAT and SMT
First-Order Subsumption via SAT Solving
Jakob Rath, Armin Biere and Laura Kovacs

BaxMC: a CEGAR approach to MAX#SAT
Thomas Vigouroux, Cristian Ene, David Monniaux, Laurent Mounier and Marie-Laure Potet

Compact Symmetry Breaking for Tournaments
Evan Lohn, Chris Lambert and Marijn Heule

Enumerative Data Types with Constraints
Andrew T Walter, David Greve and Panagiotis Manolios

Reducing NEXP-complete problems to DQBF
Fa-Hsun Chen, Shen-Chang Huang, Yu-Cheng Lu and Tony Tan

INC: A Scalable Incremental Weighted Sampler
Suwei Yang, Victor Liang and Kuldeep S. Meel

Bounded Model Checking for LLVM
Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao and Arie Gurfinkel

Parameterized Systems and Quantified Reasoning
Automatic Repair and Deadlock Detection for Parameterized Systems
Swen Jacobs, Mouhammad Sakr and Marcus Völp

Synthesizing Locally Symmetric Parameterized Protocols from Temporal Specifications
Ruoxi Zhang, Richard Trefler and Kedar Namjoshi

Synthesizing Self-Stabilizing Parameterized Protocols with Unbounded Variables
Ali Ebnenasir

The Rapid Software Verification Framework
Pamina Georgiou, Bernhard Gleiss, Ahmed Bhayat, Michael Rawson, Laura Kovacs and Giles Reger

Distributed Systems
ACORN: Network Control Plane Abstraction using Route Nondeterminism
Divya Raghunathan, Ryan Beckett, Aarti Gupta and David Walker

Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+
William Schultz, Ian Dardik and Stavros Tripakis

Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens
Bengt Jonsson, Magnus Lång and Kostis Sagonas

Synthesis
Transducers from Complex Specifications
Anvay Grover, Rüdiger Ehlers and Loris D’Antoni

Synthesis of Semantic Actions in Attribute Grammars
Pankaj Kumar Kalita, Miriyala Jeevan Kumar and Subhajit Roy

Reactive Synthesis Modulo Theories using Abstraction Refinement
Benedikt Maderbacher and Roderick Bloem

Learning Deterministic Finite Automata Decompositions from Examples and Demonstrations
Niklas Lauffer, Beyazit Yalcinkaya, Marcell Vazquez-Chanlatte, Ameesh Shah and Sanjit A. Seshia

Reachability and Safety Verification
Automated Conversion of Axiomatic to Operational Models: Theoretical and Practical Results
Adwait Godbole, Yatin A. Manerkar and Sanjit A. Seshia

Formally Verified Quite OK Image Format
Mario Bucev and Viktor Kunčak

Split Transition Power Abstraction for Unbounded Safety
Martin Blicha, Grigory Fedyukovich, Antti Hyvärinen and Natasha Sharygina

Automating Geometric Proofs of Collision Avoidance with Active Corners
Nishant Kheterpal, Elanor Tang and Jean-Baptiste Jeannin

Differential Testing of Pushdown Reachability with a Formally Verified Oracle
Anders Schlichtkrull, Morten Konggaard Schou, Jiri Srba and Dmitriy Traytel

TriCera: Verifying C Programs Using the Theory of Heaps
Zafer Esen and Philipp Ruemmer