Formal Methods in
Computer-Aided Design
October 23-27, 2023
Ames, Iowa, USA

Accepted Papers

FMCAD 2023 Accepted Papers

Authors Title Slides
Bassan, Shahaf; Amir, Guy; Corsi, Davide; Refaeli, Idan; Katz, Guy Formally Explaining Neural Networks within Reactive Systems
Li, Bohan; Cai, Shaowei Local Search For SMT On Linear and Multilinear Real Arithmetic
Lam, Kait; Coughlin, Nicholas Lift-off: Trustworthy ARMv8 semantics from formal specifications
Yu, Emily; Froleyks, Nils; Biere, Armin; Heljanko, Keijo Towards Compositional Hardware Model Checking Certification
Zhou, Yi; Bosamiya, Jay; Takashima, Yoshiki; Li, Jessica G; Heule, Marijn J.H.; Parno, Bryan Mariposa: Measuring SMT Instability in Automated Program Verification
Larraz, Daniel; Lorch, Robert M; Yahyazadeh, Moosa; Arif, M. Fareed; Chowdhury, Omar; Tinelli, Cesare CRV: An Automated Resiliency Reasoner for System Design Models
Mohamed, Abdalrhman M; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery
Meng, Baoluo; Debnath, Joyanta; Varanasi, Sarat Chandra; Manolios, Emmanuel; Durling, Michael; Paul, Saswata; Prince, Daniel; Alsabbagh, Saif; Haadsma, Richard; McMillan, Craig; Zhang, Chi; Oates, Tim Towards a Correct-by-Construction Design of Integrated Modular Avionics
Wilson, Amalee D; Noetzli, Andres P; Reynolds, Andrew; Cook, Byron; Tinelli, Cesare; Barrett, Clark Partitioning Strategies for Distributed SMT Solving
Wu, Haoze; Hahn, Christopher; Lonsing, Florian; Mann, Makai; Ramanujan, Raghuram; Barrett, Clark Lightweight Online Learning for Sets of Related Problems in Automated Reasoning
Coward, Samuel; Morini, Emiliano; Tan, Bryan; Drane, Theo; Constantinides, George Datapath Verification via Word-Level E-Graph Rewriting
Dong, Ning; Guanciale, Roberto; Dam, Mads; Lööw, Andreas Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor
Park, Kanghee; Johnson, Keith J C; D’Antoni, Loris; Reps, Thomas Modular System Synthesis
Elsaleh, Raya; Katz, Guy Delta-Debugging Neural Network Verifiers
Zhang, Changjian; Dardik, Ian; Meira-Góes, Rômulo; Garlan, David; Kang, Eunsuk Fortis: A Tool for Analysis and Repair of Robust Software Systems
Froleyks, Nils; Yu, Emily; Biere, Armin BIG Backbones
Kiesl-Reiter, Benjamin; Whalen, Michael W Proofs for Incremental SAT with Inprocessing
Codel, Cayden R; Avigad, Jeremy; Heule, Marijn J.H. Verified Encodings for SAT Solvers
Tollec, Simon; Asavoae, Mihail; Couroussé, Damien; Heydemann, Karine; Jan, Mathieu µArchiFI: Formal Modeling and Verification Strategies for Microarchitetural Fault Injections
Marmanis, Iason; Vafeiadis, Viktor Optimal Bounded Partial Order Reduction
Tafese, Joseph; Gurfinkel, Arie; Garcia-Contreras, Isabel Btor2MLIR: A Format for Hardware Verification
Taylor, Landon J; Israelsen, Bryant; Zhang, Zhen Cycle and Commute: Rare-Event Probability Verification for Chemical Reaction Networks
Bernardes Fernandes Ferreira, Nikson; Moscato, Mariano M; Titolo, Laura; Ayala-Rincon, Mauricio A provably correct floating-point implementation of Well Clear Avionics Concepts
Sakallah, Karem A; Fazekas, Katalin; Goel, Aman SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols
Ryan, Kaki; Sturton, Cynthia Countering the Path Explosion Problem in the Symbolic Execution of Hardware Designs
Qin, Xin; Hashemi, Navid; Lindemann, Lars; Deshmukh, Jyotirmoy Conformance Testing for Stochastic Cyber-Physical Systems
Godbole, Adwait; Ye, Leiqi; Manerkar, Yatin A.; Seshia, Sanjit A. Modelling and Verification of Security-Oriented Resource Partitioning Schemes
Saxena, Manasvi; Song, Shuang; Sha, Lui MediK: Towards Safe Guideline-based Clinical Decision Support
Thakkar, Arkesh H; D’Souza, Deepak Data-Driven Learning of Strong Conjunctive Invariants
Bhat, Shreesha G.; Nagar, Kartik Automating Cutoff-based Verification of Distributed Protocols
Pastva, Samuel; Henzinger, Thomas Binary decision diagrams on modern hardware