Proceedings of Formal Methods in Computer-Aided Design, FMCAD 2023

The Conference on Formal Methods in Computer-Aided Design (FMCAD) is an annual conference on the theory and applications of formal methods in hardware and system in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for reasoning formally about computing systems. FMCAD covers formal aspects of computer-aided system testing.Table of Contents: INVITED TALKS -- Reasoning about Quantifiers in SMT: The QSMA Algorithm / by Maria Paola Bonacina (p. 1) -- Distribution Testing: The New Frontier for Formal Methods / by Kuldeep Meel (p. 2) -- Formal Methods for Trusted AI / by Bettina Könighofer (p. 3) -- TUTORIALS -- Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community / by Kristin Y. Rozier, Natarajan Shankar, Cesare Tinelli, Moshe Vardi (p. 4) -- MiniZinc for Formal Methods / by Peter J. Stuckey (p. 5) -- Local Search and Its Application in CDCL/CDCL(T) solvers for SAT/SMT / by Shaowei Cai (p. 6) -- NASA’s core Flight System Framework Overview / by David Swartwout (p. 7) -- STUDENT FORUM -- The FMCAD 2022 Student Forum / by Mikoláš Janota, Nina Narodytska (p. 8) -- NEURAL NETWORKS AND MACHINE LEARNING -- Formally Explaining Neural Networks within Reactive Systems / by Shahaf Bassan, Guy Amir, Davide Corsi, Idan Refaeli, and Guy Katz (p. 10) -- Lightweight Online Learning for Sets of Related Problems in Automated Reasoning / by Haoze Wu, Christopher Hahn, Florian Lonsing, Makai Mann, Raghuram Ramanujan, and Clark Barrett (p. 23) -- DelBugV: Delta-Debugging Neural Network Verifiers / by Raya Elsaleh and Guy Katz (p. 34) -- MODEL CHECKING -- Towards Compositional Hardware Model Checking Certification / by Emily Yu, Nils Froleyks, Armin Biere, and Keijo Heljanko (p. 44) -- Btor2MLIR: A Format and Toolchain for Hardware Verification / by Joseph Tafese, Isabel Garcia-Contreras, and Arie Gurfinkel (p. 55) -- Data-Driven Learning of Strong Conjunctive Invariants / by Arkesh Thakkar and Deepak D’Souza (p. 64) -- Automating Cutoff-based Verification of Distributed Protocols / by Shreesha G. Bhat and Kartik Nagar (p. 75) -- Optimal Bounded Partial Order Reduction / by Iason Marmanis and Viktor Vafeiadis (p. 86) -- HARDWARE -- Datapath Verification via Word-Level E-Graph Rewriting / by Samuel Coward, Emiliano Morini, Bryan Tan, Theo Drane, and George A. Constantinides (p. 92) -- µArchiFI: Formal Modeling and Verification Strategies for Microarchitetural Fault Injections / by Simon Tollec, Mihail Asavoae, Damien Couroussé, Karine Heydemann, and Mathieu Jan (p. 101) -- Sylvia: Countering the Path Explosion Problem in the Symbolic Execution of Hardware Designs / by Kaki Ryan and Cynthia Sturton (p. 110) -- Binary decision diagrams on modern hardware / by Samuel Pastva and Thomas Henzinger (p. 122) -- SAT -- Proofs for Incremental SAT with Inprocessing / by Benjamin Kiesl-Reiter and Michael W. Whalen (p. 132) -- Verified Encodings for SAT Solvers / by Cayden R. Codel, Jeremy Avigad, and Marijn J. H. Heule (p. 141) -- SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols / by Katalin Fazekas, Aman Goel, and Karem A. Sakallah (p. 152) -- BIG Backbones / by Nils Froleyks, Emily Yu, and Armin Biere (p. 162) -- SMT -- Local Search For SMT On Linear and Multilinear Real Arithmetic / by Bohan Li and Shaowei Cai (p. 168) -- Mariposa: Measuring SMT Instability in Automated Program Verification / by Yi Zhou, Jay Bosamiya, Yoshiki Takashima, Jessica Li, Marijn J. H. Heule, and Bryan Parno (p. 178) -- A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery / by Abdalrhman Mohamed, Andrew Reynolds, Clark Barrett, and Cesare Tinelli (p. 189) -- Partitioning Strategies for Distributed SMT Solving / by Amalee Wilson, Andres Noetzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, and Clark Barrett (p. 199) -- AVIONICS -- CRV: An Automated Resiliency Reasoner for System Design Models / by Daniel Larraz, Robert Lorch, Moosa Yahyazadeh, M. Fareed Arif, Omar Chowdhury, and Cesare Tinelli (p. 209) -- Towards a Correct-by-Construction Design of Integrated Modular Avionics / by 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 (p. 221) -- Fortis: A Tool for Analysis and Repair of Robust Software Systems / by Changjian Zhang, Ian Dardik, Rômulo Meira-Góes, David Garlan, and Eunsuk Kang (p. 228) -- A provably correct floating-point implementation of Well Clear Avionics Concepts / by Nikson Bernardes Fernandes Ferreira, Mariano M. Moscato, Laura Titolo, and Mauricio Ayala-Rincón (p. 237) -- SECURITY AND SYNTHESIS -- Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor / by Ning Dong, Roberto Guanciale, Mads Dam, and Andreas Lööw (p. 247) -- Modular System Synthesis / by Kanghee Park, Keith J. C. Johnson, Loris D’Antoni, and Thomas Reps (p. 257) -- Modelling and Verification of Security-Oriented Resource Partitioning Schemes / by Adwait Godbole, Leiqi Ye, Yatin A. Manerkar, and Sanjit A. Seshia (p. 268) -- CYBER-PHYSICAL SYSTEMS -- Lift-off: Trustworthy ARMv8 semantics from formal specifications / by Kait Lam and Nicholas Coughlin (p. 274) -- Cycle and Commute: Rare-Event Probability Verification for Chemical Reaction Networks / by Landon Taylor, Bryant Israelsen, and Zhen Zhang (p. 284) -- Conformance Testing for Stochastic Cyber-Physical Systems / by Xin Qin, Navid Hashemi, Lars Lindemann, Jyotirmoy V. Deshmukh (p. 294) -- MediK: Towards Safe Guideline-based Clinical Decision Support / by Manasvi Saxena, Shuang Song, and Lui Sha (p. 306)Computer Science