VMCAI 2026
as the organisers put it
Online proceedings for participants are available here Welcome to the website of the 27th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2026). VMCAI provides a forum for researchers from the communities of Verification, Model Checking, and Abstract Interpretation, facilitating interaction, cross-fertilization, and advancement of hybrid methods that combine these and related areas. VMCAI 2026 will be the 27th edition in the series. VMCAI 2026 will take place during January 12-13, 2026 as a physical (in-person) event in Rennes, France, co-locate ...
who it's for
verification researchers, formal methods researchers, SMT solver developers, static analysis engineers, programming language researchers, hardware verification engineers, model checking researchers, machine learning researchers
topics
congruence closure in cvc5; transformers via logic and automata; Infer static analysis platform; termination-resilient abstract interpretation; external-memory BDD quantification; digest-driven data race detection; SMT-based probabilistic causality; proof minimization for neural network verification; delta-weakening SMT for photonics; verification of low-T quantum programs; forward symbolic execution for binary verification; formal executable semantics of PROMELA
| title | author | length |
|---|---|---|
| Producing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver | Bruno Andreotti, Haniel Barbosa | 27m |
Adapts Flatt et al.’s greedy redundant-edge algorithm into the SMT solver cvc5 and shows it produces smaller congruence explanations by keeping and weighting… | ||
| Understanding Transformers through the Lens of Logic and Automata | Anthony W. Lin | 01h 01m |
Claim: transformers without chain-of-thought map to logico-automata classes and explain why PARITY is hard; tools: reductions to circuit complexity (AC0/ATC0)… | ||
| Current State of the Industrial-Strength Infer Static Analysis Platform | David Pichardie | 01h 00m |
Infer is an industrial static analyzer with 15+ years of production use, running daily in CI against thousands of developers and 10+ million LOC with hundreds… | ||
| Termination Resilience Static Analysis | Naïm Moussaoui Remil, Caterina Urban | 30m |
Claims an abstract-interpretation framework that proves absence of robust non-termination by computing piecewise ranking functions backward over a… | ||
| Multi-variable Quantification of BDDs in External Memory using Nested Sweeping | Steffan Sølvsten, Jaco van de Pol | 30m |
Implements nested sweeping inside Adiar to do multi-variable BDD quantification in external memory, replacing recursion with coordinated concurrent sweeps and… | ||
| Data Race Detection by Digest-Driven Abstract Interpretation | Michael Schwarz, Julian Erhard | 28m |
Presents a concrete, sound definition of data races in a thread‑modular local trace semantics and implements a digest-driven abstract interpretation in Goblint… | ||
| Efficient Discovery of Actual Causality in Stochastic Systems | Arshia Rafieioskouei, Kenneth Rogale, Borzoo Bonakdarpour | 29m |
Formalizes Fenton‑Glynn probabilistic actual causality for discrete‑time Markov chains and reduces discovery to an SMT problem solved with Z3 using quantified… | ||
| Proof Minimization in Neural Network Verification | Omri Isac, Idan Refaeli, Haoze Wu, Clark Barrett, Guy Katz | 27m |
Algorithms that shrink unsat proofs from DNN verifiers by removing learned lemmas and unnecessary dependencies, implemented on the Marabou verifier and tested… | ||
| Finding Photonics Circuits via δ-weakening SMT | Marco Lewis, Benoît Valiron | 30m |
A pipeline encodes transfer matrices (bounds in [-1,1], unitarity, Fock-basis action up to amplitude α) into SMT‑LIB and runs delta-weakening SMT/dReal to get… | ||
| Atomic Gliders and Cellular Automata as Language Generators | Dana Fisman, Noa Izsak | 31m |
Defines an atomic glider as a single-cell carrier with a velocity and interaction rules, formalizes CA languages by projecting non-quiescent segments from… | ||
| Reachability in multi-agent transfer systems | Nathalie Bertrand, Loic Helouet, Engel Lefaucheux, Luca Paparazzo | 29m |
Introduces a formal model of multi-agent reachability with energy transfers, distinguishes transfer-by-groups vs global transfer and… | ||
| Efficiently Verifying Quantum Programs with Few T Gates | Youngchan Cho, Robert Rand | 29m |
Mechanized Heisenberg-style logic in the Rocq proof assistant verifies Clifford+T circuits by forwarding conjugation of polystring predicates, targeting… | ||
| Try-Mopsa: Relational Static Analysis in Your Pocket | Raphaël Monat | 27m |
A browser-only build of Mopsa compiles core OCaml components to JavaScript (gs_of_ocaml) producing a 3.1 MB bundle that runs clientsided in a web worker with… | ||
| Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification | Andreas Lindner, Karl Palmskog, Scott Constable, Mads Dam, Roberto Guanciale, Hamed Nemati | 28m |
A sound, proof-producing symbolic execution framework is formalized and implemented in HOL4 theorem prover and HolBA, instantiated for the BIR intermediate… | ||
| Verification of Generic VHDL Designs and Their Translation to Rocq | Ocan Sankur, Benoît Boyer, Florian Faissole | 31m |
Pipeline VHDL designs translate to executable Rocq functions while keeping generics uninstantiated, with automated checks that detect combinatorial loops… | ||
| Input-based Three-Valued Abstraction Refinement | Jan Onderka, Stefan Ratschan | 30m |
A new three-valued abstraction refinement framework implements input-based splitting and a simulator-like abstract state construction in the open-source tool… | ||
| Probabilistic Verification for Modular Network-on-Chip Systems | Nick Waddoups, Jonah Boe, Arnd Hartmanns, Prabal Basu, Sanghamitra Roy, Koushik Chakraborty, Zhen Zhang | 26m |
A modular NoC model written in Modest produces DTMCs and uses CTL model checking plus statistical model checking to bound power-supply-noise events up to an… | ||
| A Hybrid Meta-Learning Framework for Adaptive Safe Controller Synthesis of Dynamical(…) | Rui Guo, Yang Li, Xiuqing Cao, Wang Lin | 22m |
Proposes HyML-ASCS, a hybrid of model-based LSTM task embeddings plus gradient-based meta-learning that trains controller and barrier networks conditioned on… | ||
| A Formal Executable Semantics of PROMELA | Byoungho Son, Kyungmin Bae | 28m |
Provides an executable, interpreter-like semantics of PROMELA mechanized in the K framework and based on a new Load-and-Fire pattern over forked continuations… | ||
| nothing matches | ||