PROCEEDINGS OF THE 26TH CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN – FMCAD 2026

Contents

Tutorials
Verifying Rust Code with Verus
Travis Hance

Invited Talks
CSLib: Building a Platform for AI-assisted Formal Verification in Lean
Clark Barrett

The Parable of the Square-Dancing Witches and Wizards
Claire Xenia Wolf

The Vampire Diary
Laura Kovács

Student Forum
The FMCAD 2026 Student Forum
Tanja Schindler and Lee Barnett

SAT and MAX-SAT Solving

Verified Real-time Proof Checking for Large-Scale SAT Solving
Yong Kiam Tan, Dominik Schreiber, Johannes ̊Aman Pohjola, and Magnus O. Myreen

Weight-Aware Transformations for MaxSAT
Jesse Looney, Nikolaj Bjorner, Haoze Wu, and Nina Narodytska

Aperture: an Anytime, Complete and Incremental MaxSAT Solver
Alexander Nadel, Yam Slonimski, and Ofer Strichman

Understanding CDCL Solvers via Scalability Studies and Proofdoors
Shimin Zhang, Yechuan Xia, Chunxiao Li, Jianwen Li, Moshe Y. Vardi, and Vijay Ganesh

NobleCount: Revisiting a Forgotten Data Structure for Local Search in SAT
Yogev Shalmon, Alexander Nadel, and Ofer Strichman

SATDiv: An Effective Solver for Diverse SAT Problem
Shuangyu Lyu, Chuan Luo, Ruizhi Shi, Yuechen Duan and Chunming Hu

Decision Procedures for Arithmetic Constraints
MCSAT Modulo Transcendental Arithmetics
Jorge Gallego-Hernández, Enrico Lipparini, and Alessio Mansutti

Solving LIA⋆ Constraints Using Hilbert Bases
Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, and Clark Barrett

Randomized Satisfiability Checking for Non-Linear Arithmetic over Finite Fields
Amir Kafshdar Goharshady, Thomas Hader, Laura Kovács, and Harshit Jitendra Motwani

F-QLPs over unit relative constraints
Piotr Wojciechowski and K. Subramani

Proofs and Proof Generation
DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs
Tate Rowney, Riyaz Ahuja, Jeremy Avigad, and Sean Welleck

Proof Production for Satisfiability Modulo Finite Fields with Proof Checking in Pacheck and Lean
Pedro Saccomani, Abdalrhman Mohamed, Elizaveta Pertseva, Daniela Kaufmann, CesareTinelli, Clark Barrett, and Haniel Barbosa

Certifying Optimal MEV Strategies with Lean
Massimo Bartoletti, Riccardo Marchesin, and Roberto Zunino

IsaAbduct: A Multi-Strategy Abduction Pipeline for Isabelle/HOL
Tiago Campos, Sophie Tourret, Jasmin Blanchette, and Haniel Barbosa

Lean Certified Bitvector Solving without Bitblasting
Jan Onderka, Armin Biere, and Mathias Fleury

Optimising Constant Matrix Multiplication Circuits is NP-complete
Nicolai Fiege and Martin Lange

Parallel and Efficient Solving Strategies
Parallel SMT Solving via Dynamic Partitioning, Core-Guided Pruning, and Backbone Detection
Ilana Shapiro, Sorin Lerner, and Nikolaj Bjorner

ParaProofa: A Certifying Parallel Cube-and-Conquer QBF-Solving Framework
Cynthia Peyrer, Maximilian Heisinger, and Martina Seidl

Parallel SAT Sweeping on CNFs
Niccolò Rigi-Luperti, Armin Biere, and Dominik Schreiber

Parallelizing Congruence Closure
Zachary Kent and Amar Shah

Beyond Lemma Sharing – Novel Parallelization Strategies for PDR
Verner Vlačić

Runtime Monitoring and Specification Learning
Multi-Property Temporal Logic Monitoring
Arınç Demir and Dogan Ulus

Shrinking Mission-time LTL Runtime Monitors with Equality Saturation
Christopher Johannsen and Kristin Yvonne Rozier

Learning GR(1) Specifications from Traces
Sam Kouteili, William Fishell, Mark Santolucito, and Ruzica Piskac

Verification for Security and Privacy
SymCert: Verifying SMT-Based Policy Analyses
Emina Torlak

PolyGram: A Certifying Compiler for Network Policies
Anoud Alshnakat, Roberto Guanciale, and Mads Dam

Efficient Enumeration of Cloud Access Permissions
Lee A. Barnett, Loris D’Antoni, Amit Goel, Rami Gökhan Kıcı, Tim King, Kasper Luckow, Neha Rungta, and Yasmine Sharoda

Privacy-Preserving Robust Monitoring of Dense-Time Temporal Logic
Charles Koll, Mike Rosulek, and Houssam Abbas

Checking Information Flow in Cloud-based IoT Access Control Policies
Lorenzo Ceragioli, Letterio Galletta, and Edoardo Lunati

Specifications and Automata
Symbolic Automata for MTL∞0 with Super-Dense Semantics
Filippo Fantinato, Alessandro Cimatti, and Stefano Tonetta

On the Hierarchy of Finite-Word Hyperlanguages
Hadar Frenkel and Sarai Sheinvald

Translating LTL to Lasso Automata
Rüdiger Ehlers, Nils Hölzner, and Tobias Kühnel

Program Verification and Synthesis
Tunable Automation in Automated Program Verification
Alexander Bai, Chris Hawblitzel, and Andrea Lattuada

Verifiable Checks for Business Rule Consistency
Joseph Tafese, Arie Gurfinkel, Sam Bayless, Nick Feng, and Milad Hooshyar

Synthesis with Counterexample Guided Observational Equivalence Graphs
Guy Frankel, Rudi Schneider, Michel Steuwer, and Elizabeth Polgreen

An Extension API for the Concurrent Program Verifier Raven
Ekanshdeep Gupta and Thomas Wies

PSouffĺe: Scaling Exact Probabilistic Logic Inference for Program Analysis
Xuyang Li, Jiahao Xia, Ahmed Adnan, and Jingbo Wang

Conditional Rewrite Rule Synthesis with E-Graphs and Implication Propagation
Andrew Cheung, Chandrakana Nandi and Sorin Lerner

Model Checking and Symbolic Representation
On the Complexity of Word-Level Model Checking with Arrays
Martin Jonáš, Lea Petřivalská , and Jakub Šárnik

CB-VER: A Stable Foundation for Modular Network Control Plane Verification
Dexin Zhang, Timothy Alberdingk Thijm, David Walker, and Aarti Gupta

Certificate-Aware Property-Directed Reachability
Arman Ferdowsi and Laura Kovács

Validated Binary Decompilation Without Tears
Alicia Michael, Nicholas Coughlin, Kait Lam, and Kirsten Winter

Binary Decision Diagrams Unchained
Jaehyeok Choi and Andrew Miner

Hardware Verification
Semantics, Operations, and Properties of P3109 Floating-Point Representations in Lean
Tung-Che Chang, Sehyeok Park, Jay Lim, and Santosh Nagarakatte

Ordering-Relation Abstraction for Formal Verification of Bubble Errors in CARRY8-Based Tapped Delay Lines
Jakovs Ratners, Nikolajs Tihomorskis, and Arturs Aboltins

Certified Sequential Sweep Without Unrolling
Tobias Seufert and Christoph Scholl

Lemma Pattern Matching for SMT-based Verification of Analog Mixed-Signal Hardware
Kunal Sheth and Sara Achour

Formal Verification of Mixed-Signal Systems Using Real Number Modeling with SMT-based Model Checking
Augusto Mafra and Haniel Barbosa

Software Verification
Verifying a Memory Allocator for Rust
Sinai Kakishita, Akira Hasegawa, Toshiaki Aoki, Ryuta Kambe, and Yuuki Takano

Formal Verification of a Memory Allocator for Rust Hypervisors: From Verified to Deployable Code with Functional Equivalence Guarantees
Jun Liu, Jingxuan Liu, Shenghao Yuan, David Sanan, Kang Chen, Donggang Cao, and Yongwang Zhao

Prophecy Variables and Invariants in the Move Prover
Dao Bo Yang, Arie Gurfinkel, and Richard Trefler

Formal Verification of Imperative First-Class Functions in Move
Wolfgang Grieskamp, Teng Zhang, Vineeth Kashyap, and Jake Silverman

Multi-Threaded Software Model Checking via Parallel Trace Abstraction Refinement
Max Barth and Marie-Christine Jakobs

Planning and Reinforcement Learning
Multi-Agent Planning with Spatio-Temporal and Topological Constraints using STL-GO
Sheryl Paul, Vidisha Kudalkar, Anand Balakrishnan, Lars Lindemann, Alberto Speranzon, and Jyotirmoy Deshmukh

Requirement-Based Testing: Enhancing Reinforcement Learning with Game Theory
Ocan Sankur, Thierry Jéron, Nicolas Markey, David Mentré, and Reiya Noguchi

Probabilistic Verification and Games
dtControl 2+ε: Trading Optimality for Explainability in MDPs via Decision Trees
Tereza Kinská , Jan Křetı́nský, Tobias Meggendorfer, Sabine Rieder, and Maximilian Weininger

Property-driven Causal Abstractions for Markov Decision Processes
Jule Schmidt, Maximilian Weininger, Clemens Dubslaff, David Parker, and Nils Jansen

Conditional Sampling of Symbolic Markov Chains
Gera Weiss and Jules Zisser

Stochastic Boolean Satisfiability for Two-Player Sequential Games under Uncertainty
Chi-Kit Ng, Chih-Hsiang Chuang, and Jie-Hong R. Jiang

The Game Graph Gym
Pete Austin, Daniele Dell’Erba, and Patrick Totzke

Neural Network Verification
PICID: Proof-Driven Clause Learning in Neural Network Verification
Omri Isac, Idan Refaeli, Haoze Wu, Clark Barrett, and Guy Katz

Incremental Neural Network Verification via Learned Conflicts
Raya Elsaleh, Liam Davis, Haoze Wu, and Guy Katz

Talking with Verifiers: Automatic Specification Generation for Neural Network Verification
Yizhak Elboher, Reuven Peleg, Zhouxing Shi, Guy Katz, and Jan Křetinský

Optimized Piecewise Affine Abstractions of Neural Networks with Learnable Activation Functions
Noah Schwartz, Chandra Kanth Nagesh, Sriram Sankaranarayanan, Ramneet Kaur, Tuhin Sahai, and Susmit Jha

ML-assisted Reasoning and Verification and Proofs
Can LLMs Perform Synthesis?
Derek Egolf, Yuhao Zhou, and Stavros Tripakis

LLM-Powered Automatic Theorem Proving and Synthesis for Hybrid Systems and Games
Aditi Kabra, Jonathan Laurent, Ruben Martins, Stefan Mitsch, and André Platzer

SVAEval: An Evaluation Framework for LLM-based SVA Property Generators
Yu-An Shih, Soohyuk Cho, Aarti Gupta, and Sharad Malik

Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4
Leni Aniva, Iori Oikawa, David Dill, and Clark Barrett

Trimming Pseudo-Boolean Proofs
Berhan Oumer Adame, Bart Bogaerts, Benjamin Bogo, Simon Dold, Arthur Gontier, Wietze Koops, Ciaran McCreesh, Matthew McIlree, Jakob Nordström, Andy Oertel, Adrian Rebola-Pardo, and Mark Turnbull

Solution Space Partitioning for Extremal Set Theory
Jesse Looney, Jonah McDonald, Allison Klingler, Gloria Wu, Jonad Pulaj, and Haoze Wu