VSTTE 2025

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

October 06-07, 2025, Menlo Park, California, USA
Co-located with Formal Methods in Computer-Aided Design 2025 (FMCAD 2025)

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.

The 2025 edition of VSTTE will be the 17th international conference in the series, and will be co-located with FMCAD 2025 in Menlo Park, California, USA.

Call for papers and work-in-progress presentations

VSTTE 2025 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.

In addition to regular papers, we 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 2025 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 may be submitted via EasyChair at the VSTTE 2025 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 2025, 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

Registration

Registration to VSTTE will be part of the FMCAD registration process.

Invited talks

Design and Formal Verification of Hardware-Software Security Contracts
Caroline Trippel (Stanford University)

Virtually all hardware side-channel defenses assume the availability of microarchitectural leakage contracts, which characterize a microarchitecture's transmitters (i.e., instructions that leak at least one “unsafe” operand via hardware side-channels). Defenses against transient execution attacks, in particular, also rely microarchitectural execution contracts to characterize a microarchitecture’s control- and data-flow semantics, taking into account transient execution brought on by hardware faults or mis-predictions.

Compared to execution contracts, leakage contracts are relatively mature. Several leakage contracts have emerged in academic literature and/or industry documentation to support a variety of performant hardware side-channel defenses. However, an automated approach for formally verifying hardware adherence to a given leakage contract remains elusive. Execution contracts, on the other hand, are less well-established. In particular, it is unclear how best to restrict microarchitectural control- and data-flow so that defenses against transient execution attacks are both feasible and performant.

In this talk, I will present our work on addressing both challenges above. First, I will discuss an automated approach and tool for formally verifying that a given SystemVerilog processor design implements the leakage contract(s) it claims to. Then, I will present our work on designing a novel execution contract, which enables efficient defenses against Spectre attacks in software, and a corresponding compiler defense for hardening constant-time code (e.g., crypto code) against Spectre on hardware that satisfies it.

Formal Verification of Financial Infrastructure with Imandra
Grant Passmore (Imandra)

Many deep issues plaguing today’s financial markets are symptoms of a fundamental problem: The complexity of algorithms underlying modern finance has significantly outpaced the power of traditional tools used to design and regulate them. At Imandra, we have pioneered the application of formal verification to financial markets, and firms like Goldman Sachs, Itiviti and OneChronos rely upon Imandra’s algorithm governance tools for the design, regulation and calibration of many of their most complex algorithms. With a focus on financial infrastructure (e.g., the matching logics of national exchanges and dark pools), we will describe the landscape and illustrate our Imandra system on a number of real-world examples. We’ll sketch open problems and future directions along the way.

Invited tutorial

EasyCrypt
Pierre-Yves Strub (PQShield)

Detecting or eliminating vulnerabilities in cryptographic libraries through testing or fuzzing remains a significant challenge. This has led to the adoption of formal verification techniques to establish both functional correctness and side-channel resistance in modern cryptographic software.

In this talk, I will introduce EasyCrypt, a toolset designed to reason about relational properties in probabilistic computations involving adversarial code. EasyCrypt is particularly well-suited for constructing and verifying game-based cryptographic proofs and has been applied successfully to prove the security of sophisticated cryptographic schemes.

Although EasyCrypt facilitates reasoning at the algorithmic level, it does not directly support the development of real-world implementations. To bridge this gap, I will demonstrate how EasyCrypt integrates with the Jasmin programming language, enabling formal security guarantees for highly optimized assembly-level code.

Jasmin is tailored for "assembly-in-the-head" programming, seamlessly blending high-level constructs (like structured control flow and variables) with low-level features (such as assembly instructions and flag manipulation). In the second part of the presentation, I will offer a brief overview of Jasmin and explain how it interacts with EasyCrypt to support the formal verification of practical cryptographic implementations.

Chairs

Steering Committee

Program Chairs

Program Committee

Previous Editions