VMCAI 2025
2025-01-20..2025-01-21
Denver, United States
VMCAI ·
[VMCAI 2022, VMCAI 2023, VMCAI 2024, VMCAI 2025, VMCAI 2026]
as the organisers put it
Welcome to the website of the 26th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2025). 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 2025 will be the 25th edition in the series. VMCAI will take place during January 20-21, 2025 as a physical (in-person) event. For each accepted paper at least one author is required to register for the conference ...
| title | author | length |
|---|---|---|
| An Abstract Domain for Heap Commutativity | Jared Pincus, Eric Koskinen | 27m |
Defines an abstract domain that lifts sets of concrete heaps into pure mathematical values (e.g., lists) via a projection pi, uses a purview to mark wellformed… | ||
| A Real-Blasting Extension of Cvc5 for Reasoning about Floating-Point Arithmetic | Daisuke Ishii | 29m |
An FPA solver is implemented as an extension to Cvc5 that real-blasting — translating floating-point formulas into a real-integer arithmetic (RIA)… | ||
| Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study | Mario Bucev, Samuel Chassot, Simon Felix, Filip Schramka, Viktor Kuncak | 27m |
Adds a verified Scala backend to ASN1SCC and uses Stainless verifier to prove crash freedom and semantic properties for generated serializers. Builds a Scala… | ||
| Automated Flaw Detection for Industrial Robot RESTful Service | Yuncheng Wang, Puzhuo Liu, Yaowen Zheng, Dongliang Fang, Zhiwen Pan, Shuaizong Si, Weidong Zhang, Limin Sun | 24m |
Built a tool called RobRest that uses OpenAPI description extraction plus an LLM to pick realistic parameter values, generates dependent request sequences, and… | ||
| Parameterized Verification of Systems with Precise (0,1)-Counter Abstraction | Paul Eichler, Swen Jacobs, Chana Weil-Kennedy | 31m |
Framework that reduces parameterized systems to a finite 01 counter abstraction and proves reachability, coverability and target properties are decidable iff… | ||
| 1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via(…) | Muqsit Azeem, Debraj Chakraborty, Sudeep Kanav, Jan Kretinsky, Mohammadsadegh Mohagheghi, Stefanie Mohr, Maximilian Weininger | 04m |
Generalizes optimal policies from model-checked small instances to huge parameterized MDPs by training and pruning decision-tree learning models that predict… | ||
| Constructing Trustworthy Smart Contracts | Devora Chait-Roth, Kedar S. Namjoshi | 30m |
ASP is a new contract language plus a proof checker and a defensive compiler that guarantees absence of common bugs like overflow and reentrancy, compiles to… | ||
| Synthesis of Parametric Locally Symmetric Protocols from Abstract Temporal Specifications | Ruoxi Zhang, Richard Trefler, Kedar S. Namjoshi | 24m |
Automated procedure synthesizes an abstract representative process from a fair-CTL local specification using a modified tableau that adds interference… | ||
| ExpectAll: A BDD Based Approach for Link Failure Resilience in Elastic Optical Networks | Gustav S. Bruhns, Martin P. Hansen, Rasmus Hebsgaard, Frederik M. W. Hyldgaard, Jiri Srba | 31m |
ExpectAll encodes all Routing and Spectrum Allocation solutions into binary decision diagrams and answers failure queries orders of magnitude faster than ILP… | ||
| Formal Verification of Probabilistic Deep Reinforcement Learning Policies with(…) | Junfeng Yang, Xin Chen, Qin Li | 33m |
Formal Verification of Probabilistic Deep Reinforcement Learning Policies with Abstract Training (Video, VMCAI)
Junfeng Yang, Xin Chen, and Qin Li
(Shanghai… | ||
| Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts | Julian Erhard, Manuel Bentele, Matthias Heizmann, Dominik Klumpp, Simmo Saan, Frank Schüssele, Michael Schwarz, Helmut Seidl, Sarah Tilscher, Vesal Vojdani | 32m |
Proposes a machine-readable ghost witness format that instruments programs with ghost variables and statements so a validator checks witness validity by… | ||
| Two-way collaboration between flow and proof in SPARK | Claire Dross, Joffrey Huguet, Johannes Kanig | 29m |
SPARK (AdaCore) implements a two‑way integration where a fast interprocedural data+information flow pass runs first to emit approximated global contracts, call… | ||
| Keynote Talk: Outcome Logic: a foundational framework for concurrent and probabilistic(…) | Alexandra Silva | 01h 00m |
Presents Outcome Logic as a concrete framework that gives a compositional denotational semantics for programs mixing nondeterminism/concurrency and randomness… | ||
| Property-agnostic base case extension for scalable verification of distributed systems | Kyle Storey, Eric Mercer | 25m |
Verifies that LTL properties checked on a tiny MyCHIP cycle (one originator, one relay, one referee) extend to any-size ring by combining a Spin model checker… | ||
| LLOR: Automated Repair of OpenMP Programs | Gautam Muduganti, Utpal Bora, Saurabh Joshi, Ramakrishna Upadrasta | 28m |
LLOR is an automated repair tool for OpenMP C/C++ and Fortran programs that instruments LLVM IR, queries a data-race verifier (LLV), and uses Z3 with MaxSAT… | ||
| Abstract Local Completeness: A Local form of Abstract Non-Interference | Isabella Mastroeni | 29m |
Defines abstract local completeness as an intermediate between global completeness and per-input local completeness, formalizes it as completeness over all… | ||
| Space-Efficient Model-Checking of Higher-Order Recursion Schemes | Florian Bruse | 31m |
Shows that checking trees from tail-recursive HORS against bounded-alternation APT drops from k-EXPTIME to (k-1)-EXPSPACE complete. Achieves the upper bound by… | ||
| A Static Analysis of Entanglement | Nicola Assolini, Alessandra Di Pierro, Isabella Mastroeni | 25m |
A static analysis based on abstract interpretation constructs an abstract domain that pairs a partition of qubits with per-block value labels (classical… | ||
| Synthesis of Controllers for Continuous Blackbox Systems | Benedikt Maderbacher, Felix Windisch, Alberto Larrauri, Roderick Bloem | 28m |
Method synthesizes a continuous feed-forward controller for a stateless blackbox plant by building a linear interpolation model from a few hundred guided… | ||
| Automatic Inference of Relational Object Invariants | Yusen Su, Jorge A. Navas, Arie Gurfinkel, Isabel Garcia-Contreras | 30m |
Claims an Abstract Interpretation method that infers relational object invariants by splitting memory into banks and keeping a most-recently-used cache entry… | ||
| nothing matches | ||