Conference Series: Formal Methods in Computer-Aided Design, Volume 4

The Proceedings of the conference “Formal methods in computer-aided design 2023” provide up-to-date insight into an exciting field of research.
For the fourth time, the contributions of the conference series “Formal Methods in Computer-Aided Design” (FMCAD) are published as conference proceedings by TU Wien Academic Press. The 2023 edition of the conference series, which has been held once a year since 2006, presents the latest scientific findings in the field of computer-aided design in more than 40 contributions. The contributions cover formal aspects of computer-aided system design including verification, specification, synthesis, and testing.
The FMCAD conference, held in Ames, Iowa, USA in October 2023, is considered a leading forum in the field of computer-aided design and, since its inception, has provided an opportunity for researchers from both academia and industry to exchange ideas and to network.

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

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

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

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

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

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 2023
    Size: 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
    Added to cart.