VMCAI 2024
2024-01-15..2024-01-16
London, United Kingdom
VMCAI ·
[VMCAI 2022, VMCAI 2023, VMCAI 2024, VMCAI 2025, VMCAI 2026]
as the organisers put it
Welcome to the website of the 25th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2024). 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 2024 will be the 25th edition in the series. VMCAI will take place during January 15-16, 2024 as a physical (in-person) event. For each accepted paper at least one author is required to register for the conference ...
who it's for
model checking researchers, formal verification engineers, program analysis researchers, programming languages researchers, security engineers, embedded systems engineers, runtime verification engineers
topics
constrained Horn clause solving; quantifier elimination for Petri nets; nonlinear real arithmetic solving; speculative side-channel mitigation; abstract nonexploitability analysis; neural network verification privacy; abstraction for DNN-controlled systems; synthesis for LTL over finite traces; coalgebraic mu-calculus model checking; relational hypergraph neural networks; probabilistic program inference; automatic enforcement of Rust trait properties
| title | author | length |
|---|---|---|
| Two Projects on Human Interaction with AI | David Harel | 01h 04m |
Two short projects probe concrete effects of agent identity and a practical dev workflow. The first studies how human-or-machine identity changes behavior in… | ||
| Interpolation and Quantifiers in Ortholattices | Sankalp Gambhir, Simon Guilloud, Viktor Kuncak | 16m |
Sequent proof system for quantified orthologic is sound and complete for complete ortholattices, and validity checking runs in quadratic-time decision and… | ||
| Function synthesis for maximizing model counting | Thomas Vigouroux, Marius Bozga, Cristian Ene, Laurent Mounier | 20m |
Defines DQMax#SAT as a strict generalization of Max#SAT that subsumes DQBF and DSSAT and proves NEXPTIME-completeness, gives a concrete reduction to Max#SAT by… | ||
| Boosting Constrained Horn Solving by Unsat Core Learning | Parosh Aziz Abdulla, Chencheng Liang, Philipp Rümmer | 21m |
Built a relational hyper‑graph neural network called R-HyGNN and a framework MUSHyperNet that predicts Minimal Unsatisfiable Subsets (MUSes) of Constrained… | ||
| On the Verification of a Subgraph Construction Algorithm | Lucas Böltz, Viorica Sofronie-Stokkermans, Hannes Frey | 18m |
Automatic formalization shows the CP algorithm produces an intersection‑free connected subgraph whenever the input satisfies redundancy and coexistence by… | ||
| Efficient Local Search for Nonlinear Real Arithmetic | Zhonghan Wang, Bohua Zhan, Bohan Li, Shaowei Cai | 25m |
An efficient local-search solver for full nonlinear real arithmetic implements incremental variable scores (boundaries of make/break intervals) and temporary… | ||
| Automatic and Incremental Repair for Speculative Information Leaks | Joachim Bard, Swen Jacobs, Yakir Vizel | 20m |
CureSpec is a model-checking framework that either proves a program free of speculative side‑channel leaks or inserts concrete mitigations (fences) and emits a… | ||
| Sound Abstract Nonexploitability Analysis | Francesco Parolini, Antoine Miné | 20m |
Defines a precise nonexploitability hyperproperty and gives a sound abstract-interpretation analysis that treats user input and randomness separately, proving… | ||
| Solving Two-Player Games under Progress Assumptions | Anne-Kathrin Schmuck, K. S. Thejaswini, Irmak Saglam, Satya Prakash Nayak | 19m |
Considers augmented games (G, Φ, ψ) with Φ and ψ as LTL over vertices and shows solving them equals solving (G, ψ ⇒ Φ) but complexity depends on assumption… | ||
| Model-Guided Synthesis for LTL over Finite Traces | Shengping Xiao, Yongkang Li, Xinyue Huang, Yicong Xu, Jianwen Li, Geguang Pu, Ofer Strichman, Moshe Vardi | 16m |
MoGuS repeatedly invokes an LTLf satisfiability checker to get concrete satisfying traces, uses formula-progression to generate TDFA states on the fly, and… | ||
| Generic Model Checking for Modal Fixpoint Logics in COOL-MC | Daniel Hausmann, Merlin Humml, Simon Prucker, Lutz Schröder, Aaron Strahlberger | 13m |
COOL-MC is a model checker for coalgebraic μ-calculi that is parametric in branching type and modal operators and implements both a lazy local solver that… | ||
| Project and Conquer: Fast Quantifier Elimination for Checking Petri Nets Reacha... | Nicolas Amat, Silvano DAL ZILIO, Didier Le Botlan | 23m |
Method projects reachability queries from an original Petri net onto a reduced net by eliminating existential Presburger variables with a tailored… | ||
| Parameterized Verification of Disjunctive Timed Networks | Étienne André, Paul Eichler, Swen Jacobs, Shyam Karra | 16m |
Claim: networks of timed automata with disjunctive location guards admit a single summary TA that is language-equivalent to one process in a DTN of any size… | ||
| Resilience and Home-Space for WSTS | Alain Finkel, Mathieu Hilaire | 18m |
Paper formalizes six resilience variants (including home-space) and shows many resilience questions are undecidable for general WSTS but become decidable under… | ||
| Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic | Ritam Raha, Rajarshi Roy, Nathanaël Fijalkow, Daniel Neider, Guillermo A. Perez | 22m |
An algorithm synthesizes Metric Temporal Logic formulas that are provably bounded lookahead (future reach ≤ K) and globally separate given positive and… | ||
| TP-DejaVu: Combining Operational and Declarative Runtime Verification | Klaus Havelund, Panagiotis Katsaros, Moran Omer, Doron Peled, Anastasios Temperekidis | 15m |
Extends DejaVu with a two-phase pipeline: an operational preprocessor (Lola-like) that computes comparisons and aggregations on recent events and augments… | ||
| Automating Relational Verification of Infinite-State Programs | Hiroshi Unno | 58m |
Two automated approaches appear: a constraint-based pipeline that encodes simultaneous synthesis of a semantic scheduler and relational invariant into an… | ||
| Deductive Verification of Parameterized Embedded Systems modeled in SystemC | Philip Tasche, Raúl E. Monti, Stefanie Eva Drerup, Pauline Blohm, Paula Herber, Marieke Huisman | 21m |
Provides an automated SystemC→PVL encoding that maps SystemC processes to PVL threads, modules to shared data classes, and simulates the SystemC scheduler… | ||
| Automatically Enforcing Rust Trait Properties | Twain Byrnes, Yoshiki Takashima, Limin Jia | 10m |
A VS Code tool automatically generates trait-check harnesses and uses Kani bounded verification to assert trait invariants (equality… | ||
| Formal Runtime Error Detection During Development in the Automotive Industry | Jesko Hecking-Harbusch, Jochen Quante, Maximilian Schlund | 22m |
Module-level abstract interpretation generates a verification harness for each component, infers contracts (pre/post, array bounds, globals, init vs cyclic… | ||
| Generation of Violation Witnesses by Under-Approximating Abstract Interpretatio... | Marco Milanese, Antoine Miné | 21m |
Backwards abstract interpretation computes under-approximate sufficient preconditions, implemented as a proof-of-concept analyzer (~10k LOC) that uses a… | ||
| Correctness Witness Validation by Abstract Interpretation | Simmo Saan, Michael Schwarz, Julian Erhard, Helmut Seidl, Sarah Tilscher, Vesal Vojdani | 18m |
Introduces a concrete unassume operator that injects witness invariants into an abstract interpreter to relax state information deliberately, implemented in… | ||
| Guaranteed inference for probabilistic programs: a parallelisable, small-step o... | Michele Boreale, Luisa Collodi | 21m |
Presents a small-step operational semantics for probabilistic programs using a product of Markov kernels, handling mixed discrete/continuous distributions… | ||
| Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs | Yuxin Deng, Huiling Wu, Ming Xu | 22m |
Proposes a new quantum Hoare logic that handles hybrid classical–quantum imperative programs by modeling program states as partial density operator value… | ||
| Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Tr... | Jiaxu Tian, Dapeng Zhi, Si Liu, Peixin Wang, Guy Katz, Min Zhang | 18m |
Claims a simple engineering change: insert an abstraction layer maps reals to intervals so the network treats every interval as indistinguishable, train with… | ||
| Verification of Neural Networks’ Local Differential Classification Privacy | Roie Reshef, Anan Kabaha, Olga Seleznova, Dana Drachsler Cohen | 24m |
Defines local differential classification privacy for black-box classifiers and builds Sphynx, an algorithm that predicts an interval-based abstract “hyper… | ||
| AGNES: Abstraction-guided Framework for Deep Neural Networks Security | Akshay Dhonthi Ramesh Babu, Marcello Eiermann, Ernst Moritz Hahn, Vahid Hashemi | 11m |
AGNES is a tool that converts models to ONNX, clusters hidden neurons and stimulates cluster representatives with an artificial brain stimulation optimizer to… | ||
| Petrification: Software Model Checking for Programs with Dynamic Thread Managem... | Matthias Heizmann, Dominik Klumpp, Lars Nitzke, Frank Schüssele | 18m |
Petrification reduces C programs using pthread_create/pthread_join to a fixed-N, 1-safe Petri net model and iteratively increases N until the modeled thread… | ||
| A Fully Verified Persistency Library | Stefan Bodenmüller, John Derrick, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim | 21m |
Claims a sound, machine-checked correctness path showing that the FliT durability transformation refines an abstract PLib abstract persistency library… | ||
| A Navigation Logic for Recursive Programs with Dynamic Thread Creation | Roman Lakenbrink, Markus Müller-Olm, Christoph Ohrem, Jens Oliver Gutsfeld | 21m |
Defines NTL, a temporal logic for Dynamic Pushdown Networks that adds spawn and caller modalities to navigate thread-creation and call/return structure… | ||
| Borrowable Fractional Ownership Types for Verification | Takashi Nakayama, Yusuke Matsushita, Ken Sakayori, Ryosuke Sato, Naoki Kobayashi | 23m |
Combines ConSORT’s fractional ownership and RustHorn’s borrowable (lifetime) ownership into borrowable fractional ownership types, a flow‑sensitive type system… | ||
| nothing matches | ||