Logo Image
Formal Methods in Computer-Aided Design
© 1996 - 2026 FMCAD Association
FMCAD 2024

VSTTE 2026

18th International Conference on Verified Software: Theories, Tools and Experiments

VSTTE 2026 will be held in Graz, Austria on September 14, 2026,
co-located with Formal Methods in Computer-Aided Design 2026 (FMCAD 2026).

Overview

The goal of the VSTTE conference series is to advance the state of the art in the science and technology of software verification, through the interaction of theory development, tool evolution, and experimental validation. The Verified Software Initiative (VSI), spearheaded by Tony Hoare and Jayadev Misra, is an ambitious research program for making large-scale verified software a practical reality. The International Conference on Verified Software: Theories, Tools and Experiments (VSTTE) is the main forum for advancing the initiative. VSTTE brings together experts spanning the spectrum of software verification in order to foster international collaboration on the critical research challenges. The theoretical work includes semantic foundations and logics for specification and verification, and verification algorithms and methodologies. The tools cover specification and annotation languages, program analyzers, model checkers, interactive verifiers and proof checkers, automated theorem provers and SAT/SMT solvers, and integrated verification environments. The experimental work drives the research agenda for theory and tools by taking on significant specification/verification exercises covering hardware, operating systems, compilers, computer security, parallel computing, and cyber-physical systems.

Call for Papers and WiP Presentations

VSTTE 2026 welcomes submissions describing significant advances in the production of verified software, i.e. software that has been proved to meet its functional specifications. Submissions of theoretical, practical, and experimental contributions are equally encouraged, including those that focus on specific problems or problem domains. We are especially interested in submissions describing large-scale verification efforts that involve collaboration, theory unification, tool integration, and formalized domain knowledge. We also welcome papers describing novel experiments and case studies evaluating verification techniques and technologies.

Following its success in VSTTE 2025, we also welcome submissions on in-progress verified software projects to a “work-in-progress (presentation-only)” track. Work-in-progress contributions will not appear in the post-proceedings of the conference. Submissions describing work of interest to the software verification community, but that could not be accepted for publication in the conference proceedings, may be invited to the “work-in-progress (presentation- only)” track, on a case-by-case basis.

Topics of interest for this conference include, but are not limited to, requirements modeling, specification languages, specification/verification/ certification case studies, formal calculi, software design methods, automatic code generation, refinement methodologies, compositional analysis, verification tools (e.g., static analysis, dynamic analysis, model checking, theorem proving, satisfiability), tool integration, benchmarks, challenge problems, and integrated verification environments.

Submissions

VSTTE 2026 accepts both long (limited to 16 pages, excluding references) and short (limited to 10 pages, excluding references) paper submissions. Short submissions also cover “verification pearls” describing an elegant proof or proof technique. Submitted research papers and system descriptions must be original and not submitted for publication elsewhere.

Papers must be submitted via EasyChair at the VSTTE 2026 conference submission page.

The use of LaTeX and the Springer LNCS class files is strongly encouraged.

Submissions that are not in the proper format or are too long will not be considered.

Accepted regular-track papers will be included in the post-conference proceedings of VSTTE 2026, which will be published as a LNCS volume by Springer Verlag. Authors of those papers will have to transfer copyright of their contribution to Springer Verlag.

Important Dates

  • Abstract submission: July 10th, 2026 AoE July 17th, 2026 AoE
  • Paper submission: July 17th, 2026 AoE July 24th, 2026 AoE (firm, no further extensions)
  • Notification of acceptance: August 22nd, 2026 AoE (tentative)
  • Final pre-conference paper submission (optional): September 2nd, 2026 AoE (tentative)
  • Camera-ready for papers included in post-conference proceedings: October 23, 2026 (tentative)

Note: Authors of accepted papers at VSTTE 2025 will be able to register at early-bird rates for FMCAD/VSTTE.

Registration

Please find the information an how to register here.

VSTTE will take place in HS i1 at Inffeldgasse 18.

Program

Monday, September 14, 2026

Time Session
08:30–09:00 Coffee
09:00-10:00 Invited Talk: Roderick Bloem
Side Channel Secure Software: A Hardware Question
10:00–10:30 Coffee Break
10:30-11:30 Session 1 – Proof Assistants and Verification
10:30–10:50
Optimizing verified optimizations
Brae Webb, Ian Hayes and Mark Utting
10:50–11:10
Chartreux: Towards Verified Dataflow Analyses for Kotlin
Jacopo Philip Moretti and Marcin Wojnarowski
11:10–11:30
Formal Verification of Minimax Algorithms: A Case Study in Dafny
Wieger Wesselink, Kees Huizing and Huub van de Wetering
11:30-12:00 Session 2 – Specification Quality and Automated Repair
11:30–11:50
Automatic Repair of Network Configurations using a Modular Verifier and Symbolic Templates
Dexin Zhang, David Walker and Aarti Gupta
11:50–12:00
Failure-Proof Specification Writing: Smoke Tests in VerCors
Alexandra Jakovleva, Alexander Stekelenburg and Marieke Huisman
12:00–13:30 Lunch (Mensa, Inffeldgasse 10)
13:30-14:30 Invited Talk: Martin Jonáš
Towards a Standard Intermediate Language for Software Verification
14:30-15:10 Session 3 – AI and Verification
14:30–14:50
Synthesizing Gymnasium Environments from Structured Annotations in Differential Dynamic Logic
Thuan Cao and Stefan Mitsch
14:50–15:10
Measuring and Reducing Semantic Entropy in LTL Guardrail Generation
Rachel Papirmeister, Maria Hwang and Mark Santolucito
15:10–15:40 Coffee Break
15:40-17:00 Session 4 – Certified and Trustworthy Automated Reasoning
15:40–16:00
Verified QBF Solving in Isabelle/HOL: A Trustworthy Baseline for Mechanised Quantified Boolean Reasoning
Axel Bergström and Tjark Weber
16:00–16:20
Verified Linear Programming through Tolerance-Aware Precision Boosting
Ernesto Casablanca, Martin Sidaway, Sadegh Soudjani and Paolo Zuliani
16:20–16:40
VeriPB and CakePB 3.0: Formally Verified Pseudo-Boolean Proof Logging for General-Purpose Combinatorial Solving and Automated Reasoning Algorithms
Markus Anders, Bart Bogaerts, Benjamin Bogø, Arthur Gontier, Wietze Koops, Ciaran McCreesh, Matthew McIlree, Magnus Myreen, Jakob Nordström, Andy Oertel, Adrian Rebola-Pardo and Yong Kiam Tan
16:40–17:00
A Deeper Look at Depth: Stable Generation Accounting for Quantifier Reasoning
Can Cebeci, Nikolaj Bjørner, George Candea and Clément Pit-Claudel
17:00-18:00 In Memoriam: Tony Hoare
TBA

Tuesday, September 15, 2026

Time Session
08:30–09:00 Coffee
VSTTE Tutorial Daniela Kaufmann
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
11:00–12:30 Verification of DNNs with Marabou
12:30–14:00 Lunch (Mensa, Inffeldgasse 10)

Invited Speakers

Towards a Standard Intermediate Language for Software Verification

Martin Jonáš Masaryk University, Brno

Abstract:
Designing and implementing a software verifier is a difficult task, not only because of the complexity inherent in the verification problem itself, but also because of the challenges of handling real-world programming languages. Languages such as C and C++ have intricate syntax, and modelling their semantics correctly is highly non-trivial. This problem has been addressed by intermediate languages and verification frameworks such as Boogie, Viper, and Why3, which primarily target deductive verification. In this talk, I will present K2, the intermediate language of the software model checker Kratos2, whose goals are a syntax that is easy to parse, clear semantics, and support for both reachability and liveness properties. I will discuss its design decisions and current applications. I will then describe SV-LIB, a recent initiative that builds on K2 with the goal of designing a standard intermediate language for software verification. Besides clean syntax and semantics for verification tasks, the SV-LIB language provides native support for correctness and violation witnesses. Finally, I will report on the recent experimental use of SV-LIB in the International Competition on Software Verification (SV-COMP) and on its current status, and I will discuss future goals.

Side Channel Secure Software: A Hardware Question

Roderick Bloem Graz University of Technology

Bio:
Roderick Bloem received his M.Sc. degree in Computer Science from Leiden University, the Netherlands, in 1996, and his Ph.D. degree in Computer Science from the University of Colorado at Boulder in 2001. From 2002 until 2008, he was an Assistant at Graz University of Technology, Graz, Austria. From 2008, he has been a full professor of Computer Science at the same university; he was head of the Department of Computer Science and Biomedical Engineering from 2018 until 2023. He is a co-editor of the Handbook of Model Checking and has published over 140 peer reviewed papers in formal verification, reactive synthesis, Safe AI, and security.

Abstract:
We will present a method to prove the absence of power side channels in systems that are protected using masking. Power side channels may allow attackers to discover secret information by measuring electromagnetic emanations from a chip. Masking is a countermeasure to hide secrets by duplication and addition of randomness. We will discuss how to formally prove security against power side channel techniques for circuits. We will then move on to software running on a CPU, where hardware details can have surprising effects. We will present some vulnerabilities on a small CPU and how to fix them, and we will talk about contracts that take side channels into account.

Invited Tutorials

A Tutorial on Algebraic Verification of Arithmetic Circuits: Gröbner Bases in Practice

Daniela Kaufmann TU Wien

Bio:
Daniela Kaufmann is an FWF ESPRIT Fellow in the Research Unit Formal Methods in Systems Engineering at TU Wien Informatics. Her research combines computer algebra and automated reasoning to develop scalable verification methods for modern hardware and software systems. By integrating symbolic computation with SAT and SMT solving, she aims to make formal verification more efficient and powerful. Her work also advances certifying automated reasoning through proof logging, enabling verification results to be ultimately more trustworthy.

She received her PhD in Computer Science from Johannes Kepler University Linz, where her dissertation on the formal verification of arithmetic circuits using computer algebra was awarded the GI Dissertation Award and the Heinz Zemanek Award. She was also recognized with the Generation Future Award for Digitalization and Innovation, presented by ORF and Infineon Austria.

Abstract:
Formal verification of non-linear arithmetic circuits remains a challenging problem, and algebraic reasoning has emerged as one of the most effective approaches for tackling it. In this setting, a circuit is encoded as a system of polynomials that induces a Gröbner basis, and correctness is established by reducing a polynomial specification with respect to this basis.

This tutorial provides an introduction to algebraic arithmetic circuit verification. We will cover the necessary foundations on how circuits are modeled as polynomial systems, how Gröbner bases arise from this encoding, and how the resulting reduction procedure certifies correctness, and discuss how combinatorial reasoning can be combined with computer algebra to uncover structural information that enables simplifications difficult to obtain through purely algebraic methods.

We will then turn to one of the main bottlenecks of algebraic verification: the monomial blow-up that occurs during specification rewriting. We will present a recent approach that instead rewrites the Gröbner basis itself to expose useful linear relations, simplifying the reduction process and improving scalability. We will also touch on how proof logging can be used to certify these results.

Tutorial: Verification of DNNs with Marabou

Omri Isac Hebrew University of Jerusalem

Bio:
Omri Isac is a PhD student at the Hebrew University of Jerusalem, working on deep neural network (DNN) verification. His research primarily focuses on improving the reliability of verification through efficient proof generation and checking, as well as on complexity-theoretic aspects of DNN verification.

Abstract:
As neural networks (NNs) become a critical part of our current software, their unpredictability and opaqueness make their verification both a challenging and a crucial problem. In this tutorial, we will explore Marabou, a tool for formally verifying deep neural networks (DNNs). Formal verification aims to determine whether a DNN satisfies a given logical property, providing rigorous guarantees about its behavior.
The first part of the tutorial presents the theoretical foundations of DNN verification and an overview of Marabou’s core algorithms. The second part focuses on the practical aspects of verification: defining verification queries, specifying properties of interest, and using Marabou to verify them through its various heuristics and solving modes. Finally, time permitting, we will explore the proof-producing version of Marabou, discuss the importance of proof generation for trustworthy verification, and demonstrate how Marabou’s proofs can be independently checked.
Participants (Linux users) are encouraged to build Marabou before the tutorial (https://github.com/NeuralNetworkVerification/Marabou) and follow along.

Organization

Steering Committee

Program Chairs

Program Committee

  • Guy Amir (Cornell University)
  • Dirk Beyer (LMU Munich, Germany)
  • Roderick Bloem (Graz University of Technology)
  • Mario Carneiro (Carnegie Mellon University)
  • Zilin Chen (Nanyang Technological University)
  • Emanuele D’Osualdo (University of Konstanz)
  • Parasara Sridhar Duggirala (University of North Carolina at Chapel Hill)
  • Katalin Fazekas (TU Wien)
  • Aymeric Fromherz (Inria)
  • Arie Gurfinkel (University of Waterloo)
  • Clemens Hofstadler (Johannes Kepler University Linz)
  • Omri Isac (The Hebrew University of Jerusalem)
  • Jacques-Henri Jourdan (Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles)
  • Daniela Kaufmann (TU Wien)
  • Nian-Ze Lee (National Taiwan University)
  • Debasmita Lohar (IT University of Copenhagen)
  • Jorge A Navas (Certora)
  • Mathias Preiner (Stanford University)
  • Mark Santolucito (Barnard College)
  • Dominik Schreiber (Karlsruhe Institute of Technology)
  • Roger Su (Australian National University)
  • Emily Yu (Leiden University)
  • Stefan Zetzsche (University College London)
  • Yoni Zohar (Bar-Ilan University)
  • Tom van Dijk (University of Twente)
  • Johannes Åman Pohjola (Chalmers University)

Previous Editions