Monday, September 14, 2026
The full VSTTE program is available here: VSTTE Program.
| Time | Session | Authors |
|---|---|---|
| 08:30–09:00 | Registration | |
| Invited Talk: Roderick Bloem | ||
| 09:00–10:00 | Title TBA | |
| 10:00–10:30 | Coffee Break | |
| 12:10–13:30 | Lunch | |
| Invited Talk: Martin Jonáš | ||
| 13:30–14:30 | Title TBA | |
| 15:10–15:40 | Coffee Break | |
Tuesday, September 15, 2026
This day is Joint VSTTE/FMCAD Tutorial Day.
| Time | Session | Authors |
|---|---|---|
| 08:30–09:00 | Registration | |
| 09:00–10:00 | Coffee Break | |
| VSTTE Tutorial Daniela Kaufmann | ||
| 10:00–12:10 | A Tutorial on Algebraic Verification of Arithmetic Circuits: Gröbner Bases in Practice | |
| 12:10–13:30 | Lunch | |
| VSTTE Tutorial Omri Isac | ||
| 13:30–15:40 | Verification of DNNs with Marabou | |
| 15:40–16:00 | Coffee Break | |
| FMCAD Tutorial Travis Hance | ||
| 16:00–18:00 | Title TBA | |
| 18:00–19:30 | Reception | |
Wednesday, September 16, 2026
| Time | Track 1 | Authors | Track 2 | Authors |
|---|---|---|---|---|
| 08:30–09:00 | Registration | |||
| Invited Talk: Clark Barrett | ||||
| 09:00–10:00 | CSLib: Building a Platform for AI-assisted Formal Verification in Lean | |||
| 10:00–10:30 | Coffee Break | |||
| We Morning 1: SAT and MaxSAT SolvingWe Morning 2: Program Verification and Synthesis | ||||
| 10:30–12:10 | ||||
| Verified Real-time Proof Checking for Large-Scale SAT Solving | Yong Kiam Tan, Dominik Schreiber, Johannes Åman Pohjola and Magnus O. Myreen | Tunable Automation in Automated Program Verification | Alexander Bai, Chris Hawblitzel and Andrea Lattuada | |
| Weight-Aware Transformations for MaxSAT | Jesse Looney, Nikolaj Bjørner, Haoze Wu and Nina Narodytska | Verifiable Checks for Business Rule Consistency | Joseph Tafese, Arie Gurfinkel, Sam Bayless, Nick Feng and Milad Hooshyar | |
| Aperture: an Anytime, Complete and Incremental MaxSAT Solver | Alexander Nadel, Yam Slonimski and Ofer Strichman | Synthesis with Counterexample Guided Observational Equivalence Graphs | Guy Frankel, Rudi Schneider, Michel Steuwer and Elizabeth Polgreen | |
| Understanding CDCL Solvers via Scalability Studies and Proofdoors | Shimin Zhang, Yechuan Xia, Chunxiao Li, Jianwen Li, Moshe Y. Vardi and Vijay Ganesh | An Extension API for the Concurrent Program Verifier Raven | Ekanshdeep Gupta and Thomas Wies | |
| NobleCount: Revisiting a Forgotten Data Structure for Local Search in SAT | Yogev Shalmon, Alexander Nadel and Ofer Strichman | PSOUFFLÉ: Scaling Exact Probabilistic Logic Inference for Program Analysis (short) | Xuyang Li, Jiahao Xia, Ahmed Adnan and Jingbo Wang | |
| SATDiv: An Effective Solver for Diverse SAT Problem | Shuangyu Lyu, Chuan Luo, Ruizhi Shi, Yuechen Duan and Chunming Hu | Conditional Rewrite Rule Synthesis Using E-Graphs and Implication Propagation (short) | Andrew Cheung, Chandrakana Nandi and Sorin Lerner | |
| 12:10–13:30 | Lunch | |||
| We Afternoon 1: Planning and Reinforcement Learning | ||||
| 13:30–14:10 | ||||
| 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 | |||
| Student Forum | ||||
| 14:10–15:10 | ||||
| 15:10–16:00 | Coffee Break (with Posters) | |||
| We Late Afternoon 1: ML-assisted Reasoning and Verification + ProofsWe Late Afternoon 2: Hardware Verification | ||||
| 16:00–18:00 | ||||
| Can LLMs Perform Synthesis? | Derek Egolf, Yuhao Zhou and Stavros Tripakis | Compositional ISA-Compliance Verification of Out-of-Order RISC-V Cores | Yi-De Wu | |
| LLM-Powered Automatic Theorem Proving and Synthesis for Hybrid Systems and Games | Aditi Kabra, Jonathan Laurent, Ruben Martins, Stefan Mitsch and André Platzer | Semantics, Operations, and Properties of P3109 Floating-Point Representations in Lean | Tung-Che Chang, Sehyeok Park, Jay Lim and Santosh Nagarakatte | |
| SVAEval: An Evaluation Framework for LLM-based SVA Property Generators | Yu-An Shih, Soohyuk Cho, Aarti Gupta and Sharad Malik | Ordering-Relation Abstraction for Formal Verification of Bubble Errors in CARRY8-Based Tapped Delay Lines | Jakovs Ratners, Nikolajs Tihomorskis and Arturs Aboltins | |
| Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4 | Leni Aniva, Iori Oikawa, David Dill and Clark Barrett | Certified Sequential Sweep Without Unrolling | Tobias Seufert and Christoph Scholl | |
| 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 | Lemma Pattern Matching for SMT-based Verification of Analog Mixed-Signal Hardware | Kunal Sheth and Sara Achour | |
| Solution Space Partitioning for Extremal Set Theory | Jesse Looney, Jonah McDonald, Allison Klingler, Gloria Wu, Jonad Pulaj and Haoze Wu | Formal Verification of Mixed-Signal Systems Using Real Number Modeling with SMT-based Model Checking | 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 | Authors | Track 2 | Authors |
|---|---|---|---|---|
| 08:30–09:00 | Registration | |||
| Invited Talk: Claire Xenia Wolf | ||||
| 09:00–10:00 | Title TBA | |||
| 10:00–10:30 | Coffee Break | |||
| Th Morning 1: Neural Network VerificationTh Morning 2: Decision Procedures for Arithmetic Constraints | ||||
| 10:30–11:50 | ||||
| PICID: Proof-Driven Clause Learning in Neural Network Verification (case study) | Omri Isac, Idan Refaeli, Haoze Wu, Clark Barrett and Guy Katz | MCSAT Modulo Transcendental Arithmetics | Jorge Gallego-Hernández, Enrico Lipparini and Alessio Mansutti | |
| Incremental Neural Network Verification via Learned Conflicts | Raya Elsaleh, Liam Davis, Haoze Wu and Guy Katz | Extending an SMT Solver with LIA⋆ Constraints | Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli and Clark Barrett | |
| Talking with Verifiers: Automatic Specification Generation for Neural Network Verification | Yizhak Elboher, Reuven Peleg, Zhouxing Shi, Guy Katz and Jan Křetínský | Randomized Satisfiability Checking for Non-Linear Arithmetic over Finite Fields | Amir Kafshdar Goharshady, Thomas Hader, Laura Kovács and Harshit Jitendra Motwani | |
| 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 | F-QLPs over unit relative constraints | Piotr Wojciechowski and K. Subramani | |
| 11:50–13:10 | Lunch | |||
| Th Early Afternoon 1: Runtime Monitoring and Specification LearningTh Early Afternoon 2: Specifications and Automata | ||||
| 13:10–14:10 | ||||
| Multi-Property Temporal Logic Monitoring | Arınç Demir and Dogan Ulus | On the Hierarchy of Finite-Word Hyperlanguages | Hadar Frenkel and Sarai Sheinvald | |
| Shrinking Mission-time LTL Runtime Monitors with Equality Saturation | Christopher Johannsen and Kristin Yvonne Rozier | Symbolic Automata for MTL0,inf with Super-Dense Semantics | Filippo Fantinato, Alessandro Cimatti and Stefano Tonetta | |
| Learning GR(1) Specifications from Traces | Sam Kouteili, William Fishell, Mark Santolucito and Ruzica Piskac | Translating LTL to Lasso Automata | Rüdiger Ehlers, Nils Hölzner and Tobias Kühnel | |
| 14:10–22:00 | Social Event | |||
Friday, September 18, 2026
| Time | Track 1 | Authors | Track 2 | Authors |
|---|---|---|---|---|
| 08:30–09:00 | Registration | |||
| Invited Talk: Laura Kovács | ||||
| 09:00–10:00 | The Vampire Diary | |||
| 10:00–10:30 | Coffee Break | |||
| Fr Morning 1: Proofs and Proof GenerationFr Morning 2: Model Checking and Symbolic Representation | ||||
| 10:30–12:10 | ||||
| DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs | Tate Rowney, Riyaz Ahuja, Jeremy Avigad and Sean Welleck | On the Complexity of Word-Level Model Checking with Arrays | Martin Jonáš, Lea Petřivalská and Jakub Šárník | |
| 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 | CB-VER: A Stable Foundation for Modular Network Control Plane Verification | Dexin Zhang, Timothy Alberdingk Thijm, David Walker and Aarti Gupta | |
| Certifying optimal MEV strategies with Lean | Massimo Bartoletti, Riccardo Marchesin and Roberto Zunino | Certificate-Aware Property-Directed Reachability | Arman Ferdowsi and Laura Kovács | |
| IsaAbduct: A Multi-Strategy Abduction Pipeline for Isabelle/HOL | Tiago Campos, Sophie Tourret, Jasmin Blanchette and Haniel Barbosa | Validated Binary Decompilation Without Tears | Alicia Michael, Nicholas Coughlin, Kait Lam and Kirsten Winter | |
| Lean Certified Bitvector Solving without Bitblasting (short) | Jan Onderka, Armin Biere and Mathias Fleury | Binary Decision Diagrams Unchained | Jaehyeok Choi and Andrew Miner | |
| Optimising Constant Matrix Multiplication Circuits is NP-complete (short) | Nicolai Fiege and Martin Lange | |||
| 12:10–13:30 | Lunch | |||
| Fr Early Afternoon 1: Verification for Security and PrivacyFr Early Aftermoon 2: Software Verification | ||||
| 13:30–15:10 | ||||
| SymCert: Verifying SMT-Based Policy Analyses | Emina Torlak | Verifying a Memory Allocator for Rust | Sinai Kakishita, Akira Hasegawa, Aoki Toshiaki, Ryuta Kambe and Yuuki Takano | |
| PolyGram: A Certifying Compiler for Network Policies | Anoud Alshnakat, Roberto Guanciale and Mads Dam | 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 | |
| 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 | Prophecy Variables and Invariants in the Move Prove | Dao Bo Yang, Arie Gurfinkel and Richard Trefler | |
| Privacy-Preserving Robust Monitoring of Dense-Time Temporal Logic | Charles Koll, Houssam Abbas and Mike Rosulek | Formal Verification of Imperative First-Class Functions in Move | Wolfgang Grieskamp, Teng Zhang, Vineeth Kashyap and Jake Silverman | |
| Checking Information Flow in Cloud-based IoT Access Control Policies | Lorenzo Ceragioli, Letterio Galletta and Edoardo Lunati | Multi-Threaded Software Model Checking via Parallel Trace Abstraction Refinement | Max Barth and Marie-Christine Jakobs | |
| 15:10–15:40 | Coffee Break | |||
| Fr Late Afternoon 1: Probabilistic Verification and GamesFr Late Afternoon 2: Parallel and Efficient Solving Strategies | ||||
| 15:40–17:30 | ||||
| dtControl2+ε: Trading Optimality for Explainability in MDPs via Decision Trees | Tereza Kinská, Jan Kretinsky, Tobias Meggendorfer, Sabine Rieder and Maximilian Weininger | Parallel SMT Solving via Dynamic Partitioning, Core-Guided Pruning, and Backbone Detection | Ilana Shapiro, Sorin Lerner and Nikolaj Bjørner | |
| Property-driven Causal Abstractions for Markov Decision Processes | Jule Schmidt, Maximilian Weininger, Clemens Dubslaff, David Parker and Nils Jansen | ParaProofa: A Certifying Parallel Cube-and-Conquer QBF-Solving Framework | Cynthia Peyrer, Maximilian Heisinger and Martina Seidl | |
| Conditional Sampling of Symbolic Markov Chains | Gera Weiss and Jules Zisser | Parallel SAT Sweeping on CNFs | Niccolò Rigi-Luperti, Armin Biere and Dominik Schreiber | |
| Stochastic Boolean Satisfiability for Two-Player Sequential Games under Uncertainty | Chih-Hsiang Chuang, Chi-Kit Ng and Jie-Hong R. Jiang | Parallelizing Congruence Closure | Zachary Kent and Amar Shah | |
| The Game Graph Gym | Pete Austin, Daniele Dell'Erba and Patrick Totzke | Beyond Lemma Sharing — Novel Parallelization Strategies for PDR | Verner Vlacic | |