PROCEEDINGS OF THE 23RD CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN – FMCAD 2023

Contents

Invited Talks
Reasoning about Quantifiers in SMT: The QSMA Algorithm
Maria Paola Bonacina

Distribution Testing: The New Frontier for Formal Methods
Kuldeep Meel

Formal Methods for Trusted AI
Bettina Könighofer

Tutorials
Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community
Kristin Y. Rozier, Natarajan Shankar, Cesare Tinelli and Moshe Vardi

MiniZinc for Formal Methods
Peter J. Stuckey

Local Search and Its Application in CDCL/CDCL(T) solvers for SAT/SMT
Shaowei Cai

NASA’s core Flight System Framework Overview
David Swartwout

Student Forum
The FMCAD 2023 Student Forum
Mikoláš Janota, Nina Narodytska

Neural Networks and Machine Learning
Formally Explaining Neural Networks within Reactive Systems
Shahaf Bassan, Guy Amir, Davide Corsi, Idan Refaeli and Guy Katz

Lightweight Online Learning for Sets of Related Problems in Automated Reasoning
Haoze Wu, Christopher Hahn, Florian Lonsing, Makai Mann, Raghuram Ramanujan and Clark Barrett

DelBugV: Delta-Debugging Neural Network Verifiers
Raya Elsaleh and Guy Katz

Model Checking
Towards Compositional Hardware Model Checking Certification
Emily Yu, Nils Froleyks, Armin Biere and Keijo Heljanko

Btor2MLIR: A Format and Toolchain for Hardware Verification
Joseph Tafese, Isabel Garcia-Contreras and Arie Gurfinkel

Data-Driven Learning of Strong Conjunctive Invariants
Arkesh Thakkar and Deepak D’Souza

Automating Cutoff-based Verification of Distributed Protocols
Shreesha G. Bhat and Kartik Nagar

Optimal Bounded Partial Order Reduction
Iason Marmanis and Viktor Vafeiadis

Hardware
Datapath Verification via Word-Level E-Graph Rewriting
Samuel Coward, Emiliano Morini, Bryan Tan, Theo Drane and George A. Constantinides

μArchiFI: Formal Modeling and Verification Strategies for Microarchitetural Fault Injections
Simon Tollec, Mihail Asavoae, Damien Couroussé, Karine Heydemann and Mathieu Jan

Sylvia: Countering the Path Explosion Problem in the Symbolic Execution of Hardware Designs
Kaki Ryan and Cynthia Sturton

Binary decision diagrams on modern hardware
Samuel Pastva and Thomas Henzinger

SAT
Proofs for Incremental SAT with Inprocessing
Benjamin Kiesl-Reiter and Michael W. Whalen

Verified Encodings for SAT Solvers
Cayden R. Codel, Jeremy Avigad and Marijn J. H. Heule

SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols
Katalin Fazekas, Aman Goel and Karem A. Sakallah

BIG Backbones
Nils Froleyks, Emily Yu and Armin Biere

SMT
Local Search For SMT On Linear and Multilinear Real Arithmetic
Bohan Li and Shaowei Cai

Mariposa: Measuring SMT Instability in Automated Program
Yi Zhou, Jay Bosamiya, Yoshiki Takashima, Jessica Li, Marijn J. H. Heule and Bryan Parno

A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery
Abdalrhman Mohamed, Andrew Reynolds, Clark Barrett and Cesare Tinelli

Partitioning Strategies for Distributed SMT Solving
Amalee Wilson, Andres Noetzli, Andrew Reynolds, Byron Cook, Cesare Tinelli and Clark Barrett

Avionics
CRV: An Automated Resiliency Reasoner for System Design Models
Daniel Larraz, Robert Lorch, Moosa Yahyazadeh, M. Fareed Arif, Omar Chowdhury and Cesare Tinelli

Towards a Correct-by-Construction Design of Integrated Modular Avionic
Baoluo Meng, Joyanta Debnath, Sarat Chandra Varanasi, Emmanuel Manolios, Michael Durling, Saswata Paul, Daniel Prince, Saif Alsabbagh, Richard Haadsma, Craig McMillan, Chi Zhang and Tim Oates

Fortis: A Tool for Analysis and Repair of Robust Software Systems
Changjian Zhang, Ian Dardik, Rômulo Meira-Góes, David Garlan and Eunsuk Kang

A provably correct floating-point implementation of Well Clear Avionics Concepts
Nikson Bernardes Fernandes Ferreira, Mariano M. Moscato, Laura Titolo and Mauricio Ayala-Rincón

Security and Synthesis
Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor
Ning Dong, Roberto Guanciale, Mads Dam and Andreas Lööw

Modular System Synthesis
Kanghee Park, Keith J. C. Johnson, Loris D’Antoni and Thomas Reps

Modelling and Verification of Security-Oriented Resource Partitioning Schemes
Adwait Godbole, Leiqi Ye, Yatin A. Manerkar and Sanjit A. Seshia

Cyber-Physical Systems
Lift-off: Trustworthy ARMv8 semantics from formal specifications
Kait Lam and Nicholas Coughlin

Cycle and Commute: Rare-Event Probability Verification for Chemical Reaction Networks
Landon Taylor, Bryant Israelsen and Zhen Zhang

Conformance Testing for Stochastic Cyber-Physical Systems
Xin Qin, Navid Hashemi, Lars Lindemann and Jyotirmoy V. Deshmukh

MediK: Towards Safe Guideline-based Clinical Decision Support
Manasvi Saxena, Shuang Song and Lui Sha