Formal Methods in
Computer-Aided Design
Oct 17—21, 2022
Trento, Italy

Accepted Papers

Authors Title Slides
Yannan Li, Jingbo Wang and Chao Wang Proving Robustness of KNNs Against Adversarial Data Poisoning Slides
Swen Jacobs, Mouhammad Sakr and Marcus Völp Automatic Repair and Deadlock Detection for Parameterized Systems Slides
Pamina Georgiou, Bernhard Gleiss, Ahmed Bhayat, Michael Rawson, Laura Kovacs and Giles Reger The Rapid Software Verification Framework Slides
Randal Bryant TBUDDY: A Proof-Generating BDD Package Slides
Andreas Lööw Reconciling Verified-Circuit Development and Verilog Development Slides
Emily Yu, Nils Frolyeks, Armin Biere and Keijo Heljanko Stratified Certification for k-Induction Slides
Anders Schlichtkrull, Morten Konggaard Schou, Jiri Srba and Dmitriy Traytel Differential Testing of Pushdown Reachability with a Formally Verified Oracle Slides
Anvay Grover, Rüdiger Ehlers and Loris D'Antoni Synthesizing Transducers from Complex Specifications Slides
Omri Isac, Clark Barrett, Min Zhang and Guy Katz Neural Network Verification with Proof Production Slides
Thomas Vigouroux, Cristian Ene, David Monniaux, Laurent Mounier and Marie-Laure Potet BaxMC: a CEGAR approach to MAX#SAT Slides
Tom Zelazny, Haoze Wu, Clark Barrett and Guy Katz On Optimizing Back-Substitution Methods for Neural Network Verification Slides
Roope Kaivola and Neta Bar Kama Timed Causal Fanin Analysis for Symbolic Circuit Simulation Slides
Divya Raghunathan, Ryan Beckett, Aarti Gupta and David Walker ACORN: Network Control Plane Abstraction using Route Nondeterminism Slides
Pankaj Kumar Kalita, Miriyala Jeevan Kumar and Subhajit Roy Synthesis of Semantic Actions in Attribute Grammars Slides
Mario Bucev and Viktor Kunčak Formally Verified Quite OK Image Format Slides
Guy Amir, Tom Zelazny, Guy Katz and Michael Schapira Verification-Aided Deep Ensemble Selection Slides
William Schultz, Ian Dardik and Stavros Tripakis Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+ Slides
Alexander Konrad, Christoph Scholl, Alireza Mahzoon, Daniel Große and Rolf Drechsler Divider Verification Using Symbolic Computer Algebra and Delayed Don’t Care Optimization Slides
Ruoxi Zhang, Richard Trefler and Kedar Namjoshi Synthesizing Locally Symmetric Parameterized Protocols from Temporal Specifications Slides
Jonas Haglund and Roberto Guanciale Formally Verified Isolation of DMA Slides
Aarti Gupta, Roope Kaivola, Mihir Parang Mehta and Vaibhav Singh Error Correction Code Algorithm and Implementation Verification using Symbolic Representations Slides
Andres Noetzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Cesare Tinelli and Clark Barrett Reconstructing Fine-Grained Proofs of Complex Rewrites Using a Domain-Specific Language Slides
Ali Ebnenasir Synthesizing Self-Stabilizing Parameterized Protocols with Unbounded Variables Slides
Bengt Jonsson, Magnus Lång and Kostis Sagonas Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens Slides
Oliver Flatt, Samuel Coward, Max Willsey, Zachary Tatlock and Pavel Panchekha Small Proofs from Congruence Closure Slides
Evan Lohn, Chris Lambert and Marijn Heule Compact Symmetry Breaking for Tournaments Slides
Adwait Godbole, Yatin A. Manerkar and Sanjit A. Seshia Automated Conversion of Axioms to Operational Models: Theoretical and Practical Results Slides
Fa-Hsun Chen, Shen-Chang Huang, Yu-Cheng Lu and Tony Tan Reducing NEXP-complete problems to DQBF Slides
Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao and Arie Gurfinkel Bounded Model Checking for LLVM Slides
Martin Blicha, Grigory Fedyukovich, Antti Hyvärinen and Natasha Sharygina Split Transition Power Abstraction for Unbounded Safety Slides
Abhishek Nair, Saranyu Chattopadhyay, Haoze Wu, Alex Ozdemir and Clark Barrett Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers Slides
Suwei Yang, Victor Liang and Kuldeep S. Meel INC: A Scalable Incremental Weighted Sampler Slides
Niklas Lauffer, Beyazit Yalcinkaya, Marcell Vazquez-Chanlatte, Ameesh Shah and Sanjit A. Seshia Learning Deterministic Finite Automata Decompositions from Examples and Demonstrations Slides
Nishant Kheterpal, Elanor Tang and Jean-Baptiste Jeannin Automating Geometric Proofs of Collision Avoidance with Active Corners Slides
Andrew T Walter, David Greve and Panagiotis Manolios Enumerative Data Types with Constraints Slides
Ross Daly, Caleb Donovick, Jack Melchert, Raj Setaluri, Nestan Tsiskaridze, Priyanka Raina, Clark Barrett and Pat Hanrahan Synthesizing Instruction Selection Rewrite Rules from RTL using SMT Slides
Zafer Esen and Philipp Ruemmer TriCera: Verifying C Programs Using the Theory of Heaps Slides
Karl Palmskog, Xiaomo Yao, Ning Dong, Roberto Guanciale and Mads Dam Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution Slides
Benedikt Maderbacher and Roderick Bloem Reactive Synthesis Modulo Theories using Abstraction Refinement Slides
Jakob Rath, Armin Biere and Laura Kovacs First-Order Subsumption via SAT Solving Slides