FMCAD 2026 Program

Sessions take place in the following rooms:

SLab = Schumpeter Lecture Hall, Inffeldgasse 11, 3rd Floor
HS i9 = Inffeldgasse 13
HS i1 = Inffeldgasse 18

Mon 14 Tue 15 Wed 16 Thu 17 Fri 18

Monday, September 14, 2026

The full VSTTE program is available here: VSTTE Program.

Time	Session
08:30–09:00	Coffee
Invited Talk: Roderick Bloem (HS i1)
09:00–10:00	Side Channel Secure Software: A Hardware Question
10:00–10:30	Coffee Break
10:30–12:00	VSTTE
12:00–13:30	Lunch (Mensa, Inffeldgasse 10)
Invited Talk: Martin Jonáš (HS i1)
13:30–14:30	Towards a Standard Intermediate Language for Software Verification
14:30–15:10	VSTTE
15:10–15:40	Coffee Break
15:40–17:00	VSTTE
In Memoriam: Tony Hoare (HS i1)
17:00–18:00	TBA

Tuesday, September 15, 2026

This day is a joint VSTTE and FMCAD Tutorial day.

Time	Session
08:30–09:00	Coffee
VSTTE Tutorial Daniela Kaufmann (HS i1)
09:00–10:30	A Tutorial on Algebraic Verification of Arithmetic Circuits: Gröbner Bases in Practice
10:30–11:00	Coffee Break
VSTTE Tutorial Omri Isac (HS i1)
11:00–12:30	Verification of DNNs with Marabou
12:30–14:00	Lunch (Mensa, Inffeldgasse 10)
FMCAD Tutorial Travis Hance (HS i1)
14:00–16:00	Verifying Rust code with Verus
16:00–18:00	Welcome Reception VSTTE & FMCAD Blauer Platz, Inffeldgasse 11
18:30	City Tour^*

Wednesday, September 16, 2026

Time	Track 1 – SLab	Track 2 – HS i9
08:30–09:00	Coffee
Invited Talk: Clark Barrett (SLab)
09:00–10:00	CSLib: Building a Platform for AI-assisted Formal Verification in Lean
10:00–10:30	Coffee Break
10:30–12:10	Wednesday Morning 1: SAT and MaxSAT Solving Wednesday Morning 2: Program Verification and Synthesis
	10:30–10:40 Verified Real-time Proof Checking for Large-Scale SAT Solving (short) Yong Kiam Tan, Dominik Schreiber, Johannes Åman Pohjola and Magnus O. Myreen	10:30–10:50 Tunable Automation in Automated Program Verification Alexander Bai, Chris Hawblitzel and Andrea Lattuada
	10:40–11:00 Weight-Aware Transformations for MaxSAT Jesse Looney, Nikolaj Bjørner, Haoze Wu and Nina Narodytska	10:50–11:10 Verifiable Checks for Business Rule Consistency Joseph Tafese, Arie Gurfinkel, Sam Bayless, Nick Feng and Milad Hooshyar
	11:00–11:10 Aperture: an Anytime, Complete and Incremental MaxSAT Solver (short) Alexander Nadel, Yam Slonimski and Ofer Strichman	11:10–11:30 Synthesis with Counterexample Guided Observational Equivalence Graphs Guy Frankel, Rudi Schneider, Michel Steuwer and Elizabeth Polgreen
	11:10–11:30 Understanding CDCL Solvers via Scalability Studies and Proofdoors Shimin Zhang, Yechuan Xia, Chunxiao Li, Jianwen Li, Moshe Y. Vardi and Vijay Ganesh	11:30–11:50 An Extension API for the Concurrent Program Verifier Raven Ekanshdeep Gupta and Thomas Wies
	11:30–11:40 NobleCount: Revisiting a Forgotten Data Structure for Local Search in SAT (short) Yogev Shalmon, Alexander Nadel and Ofer Strichman	11:50–12:00 PSOUFFLÉ: Scaling Exact Probabilistic Logic Inference for Program Analysis (short) Xuyang Li, Jiahao Xia, Ahmed Adnan and Jingbo Wang
	11:40–11:50 SATDiv: An Effective Solver for Diverse SAT Problem (short) Shuangyu Lyu, Chuan Luo, Ruizhi Shi, Yuechen Duan and Chunming Hu	12:00–12:10 Conditional Rewrite Rule Synthesis Using E-Graphs and Implication Propagation (short) Andrew Cheung, Chandrakana Nandi and Sorin Lerner
12:10–13:30	Lunch (Mensa, Inffeldgasse 10)
13:30–14:10	Wednesday Afternoon 1: Planning and Reinforcement Learning
	13:30–13:50 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
	13:50–14:10 Requirement-Based Testing: Enhancing Reinforcement Learning with Game Theory Ocan Sankur, Thierry Jéron, Nicolas Markey, David Mentré and Reiya Noguchi
14:10–15:10	Student Forum (SLab)
15:10–16:00	Coffee Break (with Posters)
16:00–18:00	Wednesday Late Afternoon 1: ML-assisted Reasoning and Verification + Proofs Wednesday Late Afternoon 2: Hardware Verification
	16:00–16:20 Can LLMs Perform Synthesis? Derek Egolf, Yuhao Zhou and Stavros Tripakis
	16:20–16:40 LLM-Powered Automatic Theorem Proving and Synthesis for Hybrid Systems and Games Aditi Kabra, Jonathan Laurent, Ruben Martins, Stefan Mitsch and André Platzer	16:00–16:20 Semantics, Operations, and Properties of P3109 Floating-Point Representations in Lean Tung-Che Chang, Sehyeok Park, Jay Lim and Santosh Nagarakatte
	16:40–17:00 SVAEval: An Evaluation Framework for LLM-based SVA Property Generators Yu-An Shih, Soohyuk Cho, Aarti Gupta and Sharad Malik	16:20–16:40 Ordering-Relation Abstraction for Formal Verification of Bubble Errors in CARRY8-Based Tapped Delay Lines Jakovs Ratners, Nikolajs Tihomorskis and Arturs Aboltins
	17:00–17:20 Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4 Leni Aniva, Iori Oikawa, David Dill and Clark Barrett	16:40–17:00 Certified Sequential Sweep Without Unrolling Tobias Seufert and Christoph Scholl
	17:20–17:40 Trimming Pseudo-Boolean Proofs Berhan Oumer Adame, Bart Bogaerts, Benjamin Bogø, Simon Dold, Arthur Gontier, Wietze Koops, Ciaran McCreesh, Matthew McIlree, Jakob Nordström, Andy Oertel, Adrian Rebola-Pardo and Mark Turnbull	17:00–17:20 Lemma Pattern Matching for SMT-based Verification of Analog Mixed-Signal Hardware Kunal Sheth and Sara Achour
	17:40–18:00 Solution Space Partitioning for Extremal Set Theory Jesse Looney, Jonah McDonald, Allison Klingler, Gloria Wu, Jonad Pulaj and Haoze Wu	17:20–17:30 Formal Verification of Mixed-Signal Systems Using Real Number Modeling with SMT-based Model Checking (short) Augusto Mafra and Haniel Barbosa
Business Meeting
18:00–19:00	Details TBA
19:30–22:00	PC Dinner

Thursday, September 17, 2026

Time	Track 1 – SLab	Track 2 – HS i9
08:30–09:00	Coffee
Invited Talk: Claire Xenia Wolf (SLab)
09:00–10:00	The Parable of the Square-Dancing Witches and Wizards
10:00–10:30	Coffee Break
10:30–11:50	Thursday Morning 1: Neural Network Verification Thursday Morning 2: Decision Procedures for Arithmetic Constraints
	10:30–10:50 PICID: Proof-Driven Clause Learning in Neural Network Verification Omri Isac, Idan Refaeli, Haoze Wu, Clark Barrett and Guy Katz	10:30–10:50 MCSAT Modulo Transcendental Arithmetics Jorge Gallego-Hernández, Enrico Lipparini and Alessio Mansutti
	10:50–11:10 Incremental Neural Network Verification via Learned Conflicts Raya Elsaleh, Liam Davis, Haoze Wu and Guy Katz	10:50–11:10 Extending an SMT Solver with LIA⋆ Constraints Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli and Clark Barrett
	11:10–11:20 Talking with Verifiers: Automatic Specification Generation for Neural Network Verification (short) Yizhak Elboher, Reuven Peleg, Zhouxing Shi, Guy Katz and Jan Křetínský	11:10–11:30 Randomized Satisfiability Checking for Non-Linear Arithmetic over Finite Fields Amir Kafshdar Goharshady, Thomas Hader, Laura Kovács and Harshit Jitendra Motwani
	11:20–11:40 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	11:30–11:50 F-QLPs over unit relative constraints Piotr Wojciechowski and K. Subramani
11:50–13:10	Lunch (Mensa, Inffeldgasse 10)
13:10–14:10	Thursday Early Afternoon 1: Runtime Monitoring and Specification Learning Thursday Early Afternoon 2: Specifications and Automata
	13:10–13:30 Multi-Property Temporal Logic Monitoring Arınç Demir and Dogan Ulus	13:10–13:30 On the Hierarchy of Finite-Word Hyperlanguages Hadar Frenkel and Sarai Sheinvald
	13:30–13:50 Shrinking Mission-time LTL Runtime Monitors with Equality Saturation Christopher Johannsen and Kristin Yvonne Rozier	13:30–13:50 Symbolic Automata for MTL0,inf with Super-Dense Semantics Filippo Fantinato, Alessandro Cimatti and Stefano Tonetta
	13:50–14:00 Learning GR(1) Specifications from Traces (short) Sam Kouteili, William Fishell, Mark Santolucito and Ruzica Piskac	13:50–14:00 Translating LTL to Lasso Automata (short) Rüdiger Ehlers, Nils Hölzner and Tobias Kühnel
14:10–22:00	Social Event Bus trip to the countryside! We take off from Blauer Platz, Inffeldgasse 13

Friday, September 18, 2026

Time	Track 1 – SLab	Track 2 – HS i9
08:30–09:00	Coffee
Invited Talk: Laura Kovács (SLab)
09:00–10:00	The Vampire Diary
10:00–10:30	Coffee Break
10:30–12:10	Friday Morning 1: Proofs and Proof Generation Friday Morning 2: Model Checking and Symbolic Representation
	10:30–10:50 DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs Tate Rowney, Riyaz Ahuja, Jeremy Avigad and Sean Welleck	10:30–10:50 On the Complexity of Word-Level Model Checking with Arrays Martin Jonáš, Lea Petřivalská and Jakub Šárník
	10:50–11:10 Proof Production for Satisfiability Modulo Finite Fields with Proof Checking in Pacheck and Lean Pedro Saccomani, Abdalrhman Mohamed, Elizaveta Pertseva, Daniela Kaufmann, Cesare Tinelli, Clark Barrett and Haniel Barbosa	10:50–11:10 CB-VER: A Stable Foundation for Modular Network Control Plane Verification Dexin Zhang, Timothy Alberdingk Thijm, David Walker and Aarti Gupta
	11:10–11:30 Certifying optimal MEV strategies with Lean Massimo Bartoletti, Riccardo Marchesin and Roberto Zunino	11:10–11:30 Certificate-Aware Property-Directed Reachability Arman Ferdowsi and Laura Kovács
	11:30–11:50 IsaAbduct: A Multi-Strategy Abduction Pipeline for Isabelle/HOL Tiago Campos, Sophie Tourret, Jasmin Blanchette and Haniel Barbosa	11:30–11:50 Validated Binary Decompilation Without Tears Alicia Michael, Nicholas Coughlin, Kait Lam and Kirsten Winter
	11:50–12:00 Lean Certified Bitvector Solving without Bitblasting (short) Jan Onderka, Armin Biere and Mathias Fleury	11:50–12:10 Binary Decision Diagrams Unchained Jaehyeok Choi and Andrew Miner
	12:00–12:10 Optimising Constant Matrix Multiplication Circuits is NP-complete (short) Nicolai Fiege and Martin Lange
12:10–13:30	Lunch (Mensa, Inffeldgasse 10)
13:30–15:10	Friday Early Afternoon 1: Verification for Security and Privacy Fr Early Aftermoon 2: Software Verification
	13:30–13:50 SymCert: Verifying SMT-Based Policy Analyses Emina Torlak	13:30–13:50 Verifying a Memory Allocator for Rust Sinai Kakishita, Akira Hasegawa, Aoki Toshiaki, Ryuta Kambe and Yuuki Takano
	13:50–14:10 PolyGram: A Certifying Compiler for Network Policies Anoud Alshnakat, Roberto Guanciale and Mads Dam	13:50–14:10 Formal Verification of a Memory Allocator for Rust Hypervisors: From Verified to Deployable Code with Functional Equivalence Guarantees Liu Jun, Liu Jingxuan, Shenghao Yuan, David Sanan, Chen Kang, Cao Donggang and Yongwang Zhao
	14:10–14:30 Efficient Enumeration of Cloud Access Permissions Lee Barnett, Loris D'Antoni, Amit Goel, Rami Gökhan Kıcı, Tim King, Kasper Luckow, Neha Rungta and Yasmine Sharoda	14:10–14:30 Prophecy Variables and Invariants in the Move Prover Dao Bo Yang, Arie Gurfinkel and Richard Trefler
	14:30–14:50 Privacy-Preserving Robust Monitoring of Dense-Time Temporal Logic Charles Koll, Houssam Abbas and Mike Rosulek	14:30–14:50 Formal Verification of Imperative First-Class Functions in Move Wolfgang Grieskamp, Teng Zhang, Vineeth Kashyap and Jake Silverman
	14:50–15:10 Checking Information Flow in Cloud-based IoT Access Control Policies Lorenzo Ceragioli, Letterio Galletta and Edoardo Lunati	14:50–15:10 Multi-Threaded Software Model Checking via Parallel Trace Abstraction Refinement Max Barth and Marie-Christine Jakobs
15:10–15:40	Coffee Break
15:40–17:30	Friday Late Afternoon 1: Probabilistic Verification and Games Friday Late Afternoon 2: Parallel and Efficient Solving Strategies
	15:40–16:00 dtControl2+ε: Trading Optimality for Explainability in MDPs via Decision Trees Tereza Kinská, Jan Kretinsky, Tobias Meggendorfer, Sabine Rieder and Maximilian Weininger	15:40–16:00 Parallel SMT Solving via Dynamic Partitioning, Core-Guided Pruning, and Backbone Detection Ilana Shapiro, Sorin Lerner and Nikolaj Bjørner
	16:00–16:20 Property-driven Causal Abstractions for Markov Decision Processes Jule Schmidt, Maximilian Weininger, Clemens Dubslaff, David Parker and Nils Jansen	16:00–16:10 ParaProofa: A Certifying Parallel Cube-and-Conquer QBF-Solving Framework (short) Cynthia Peyrer, Maximilian Heisinger and Martina Seidl
	16:20–16:40 Conditional Sampling of Symbolic Markov Chains Gera Weiss and Jules Zisser	16:10–16:20 Parallel SAT Sweeping on CNFs (short) Niccolò Rigi-Luperti, Armin Biere and Dominik Schreiber
	16:40–17:00 Stochastic Boolean Satisfiability for Two-Player Sequential Games under Uncertainty Chih-Hsiang Chuang, Chi-Kit Ng and Jie-Hong R. Jiang	16:20–16:40 Parallelizing Congruence Closure Zachary Kent and Amar Shah
	17:00–17:10 The Game Graph Gym (short) Pete Austin, Daniele Dell'Erba and Patrick Totzke	16:40–17:00 Beyond Lemma Sharing — Novel Parallelization Strategies for PDR Verner Vlacic
18:00–??:??	Board Games^*

^* Optional and free of charge.