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

Accepted Papers

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