PROCEEDINGS OF THE 23RD CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN – FMCAD 2023
Conference Series: Formal Methods in Computer-Aided Design, Volume 4
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
Product information
Publication date: October 2023Size: 332 pages
Format: 24 x 17 cm
Language: Englisch
DOI: 10.34727/2023/isbn.978-3-85448-060-0
ISBN (E-Book): 978-3-85448-060-0