PROCEEDINGS OF THE 22ND CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN – FMCAD 2022
Conference Series: Formal Methods in Computer-Aided Design, Volume 3
The third volume of proceedings of the conference series on ‘Formal methods in computer-aided design’ offers new insights into an exciting field of research.
For the third time, TU Wien Academic Press is publishing the conference proceedings of the conference series ‘Formal Methods in Computer-Aided Design’, FMCAD. The present volume in the conference series, held annually since 2006, includes over 40 conference papers presenting the most recent scientific findings in the field of computer-aided design. The papers cover a wide variety of topics including verification, testing and synthesis of models and systems as well as applications of AI-based methods.
The 22nd FMCAD conference is held in October 2022 in Italy. The conference series is regarded as the leading forum in the field of computer-aided design, and offers researchers from both academic and industrial settings opportunities for scientific exchange and networking.
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
Product information
Publication date: October 2022Size: 405 pages
Format: 24 x 17 cm
Language: Englisch
DOI: 10.34727/2022/isbn.978-3-85448-053-2
ISBN (E-Book): 978-3-85448-053-2