| 2023 | Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor. | Ning Dong, Roberto Guanciale, Mads Dam, Andreas Lw |
| 2023 | Datapath Verification via Word-Level E-Graph Rewriting. | Samuel Coward, Emiliano Morini, Bryan Tan, Theo Drane, George A. Constantinides |
| 2023 | Verified Encodings for SAT Solvers. | Cayden R. Codel, Jeremy Avigad, Marijn J. H. Heule |
| 2023 | Local Search and Its Application in CDCL/CDCL(T) solvers for SAT/SMT. | Shaowei Cai |
| 2023 | Reasoning about Quantifiers in SMT: The QSMA algorithm. | Maria Paola Bonacina |
| 2023 | Automating Cutoff-based Verification of Distributed Protocols. | Shreesha G. Bhat, Kartik Nagar |
| 2023 | Formally Explaining Neural Networks within Reactive Systems. | Shahaf Bassan, Guy Amir, Davide Corsi, Idan Refaeli, Guy Katz |
| 2022 | Synthesizing Locally Symmetric Parameterized Protocols from Temporal Specifications. | Ruoxi Zhang, Richard J. Trefler, Kedar S. Namjoshi |
| 2022 | On Optimizing Back-Substitution Methods for Neural Network Verification. | Tom Zelazny, Haoze Wu, Clark W. Barrett, Guy Katz |
| 2022 | Stratified Certification for k-Induction. | Emily Yu, Nils Froleyks, Armin Biere, Keijo Heljanko |
| 2022 | INC: A Scalable Incremental Weighted Sampler. | Suwei Yang, Victor C. Liang, Kuldeep S. Meel |
| 2022 | Enumerative Data Types with Constraints. | Andrew T. Walter, David A. Greve, Panagiotis Manolios |
| 2022 | BaxMC: a CEGAR approach to Max#SAT. | Thomas Vigouroux, Cristian Ene, David Monniaux, Laurent Mounier, Marie-Laure Potet |
| 2022 | Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA | William Schultz, Ian Dardik, Stavros Tripakis |
| 2022 | Differential Testing of Pushdown Reachability with a Formally Verified Oracle. | Anders Schlichtkrull, Morten Konggaard Schou, Jir Srba, Dmitriy Traytel |
| 2022 | First-Order Subsumption via SAT Solving. | Jakob Rath, Armin Biere, Laura Kovcs |
| 2022 | ACORN: Network Control Plane Abstraction using Route Nondeterminism. | Divya Raghunathan, Ryan Beckett, Aarti Gupta, David Walker |
| 2022 | Bounded Model Checking for LLVM. | Siddharth Priya, Yusen Su, Yuyan Bao, Xiang Zhou, Yakir Vizel, Arie Gurfinkel |
| 2022 | The FMCAD 2022 Student Forum. | Mathias Preiner |
| 2022 | Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution. | Karl Palmskog, Xiaomo Yao, Ning Dong, Roberto Guanciale, Mads Dam |
| 2022 | Verification of Distributed Protocols: Decidable Modeling and Invariant Inference. | Oded Padon |
| 2022 | Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. | Andres Ntzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2022 | Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers. | Abhishek Anil Nair, Saranyu Chattopadhyay, Haoze Wu, Alex Ozdemir, Clark W. Barrett |
| 2022 | Reactive Synthesis Modulo Theories using Abstraction Refinement. | Benedikt Maderbacher, Roderick Bloem |
| 2022 | Reconciling Verified-Circuit Development and Verilog Development. | Andreas Lw |