VMCAI 2022
2022-01-16..2022-01-18
-- online --
VMCAI ·
[VMCAI 2022, VMCAI 2023, VMCAI 2024, VMCAI 2025, VMCAI 2026]
as the organisers put it
Welcome to the website of the 23rd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2022). 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 2022 will be the 23rd edition in the series. VMCAI will take place during January 16-18, 2022. Invited Speakers Işil DilligUT Austin Javier EsparzaTU Munich Thomas A. HenzingerIST Austria Videos of Talks You can f ...
| title | author | length |
|---|---|---|
| Sequential Information Flow | Thomas A. Henzinger | 57m |
Introduces Hypertrace Logic, a first-order array-style logic with explicit trace vs time quantifiers and shows that HyperLTL (trace-prefix fragment) cannot… | ||
| Relational String Abstract Domains | Vincenzo Arceri, Martina Olliaro, Agostino Cortesi, Pietro Ferrara | 30m |
Defines a constructive framework that turns any pre/partial string order into a relational abstract domain, instantiates it for substring, character inclusion… | ||
| Lightweight Shape Analysis based on Physical Types | Olivier Nicole, Matthieu Lemerre, Xavier Rival | 27m |
Defines a new abstract-interpretation memory analysis that summarizes the heap with physical types encoding byte-level layouts and pairs that with a focusing… | ||
| A Flow-Insensitive-Complete Program Representation | Solene Mirliaz, David Pichardie | 29m |
Claims a program transformation that makes a flow‑insensitive analysis as precise as a flow‑sensitive one for assertion failures under pure collecting… | ||
| Verifying Pufferfish Privacy in Hidden Markov Models | Depeng Liu, Bow-Yaw Wang, Lijun Zhang | 29m |
Proposes encoding discrete privacy mechanisms as hidden Markov models and reduces Pufferfish verification to SMT solving, proving the decision problem NP-hard… | ||
| Verifying Solidity Smart Contracts Via Communication Abstraction in SmartACE | Scott Wesley, Maria Christakis, Jorge A. Navas, Richard Trefler, Valentin Wu?stholz, Arie Gurfinkel | 30m |
SmartACE is an automated pipeline that translates Solidity + Scribble specs to an LLVM harness and applies parametrized verification via local bundle… | ||
| Generalized Arrays for Stainless Frames | Georg Stefan Schmid, Viktor Kuncak | 29m |
Implements a verification pipeline in Stainless (Scala) that encodes dynamic frames without quantifiers by lowering heaps to arrays and emitting Z3’s extended… | ||
| NP Satisfiability for Arrays as Powers | Rodrigo Raya, Viktor Kunc?ak | 27m |
Claim: the existential satisfiability problem for product (power) structures with an equicardinality predicate is in NP. Proof uses a semantic, model-theoretic… | ||
| Bit-Precise Reasoning via Int-Blasting | Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Notzli, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli | 30m |
Introduces int-blasting: translating bit-vector formulas to integer arithmetic plus uninterpreted functions and implementing four variants (eager/lazy ×… | ||
| Back to the Future: A Fresh Look at Linear Temporal Logic | Javier Esparza | 01h 07m |
Claims a single-exponential normalization for LTL (instead of the old non‑elementary blowup), gives rewrite rules that push GF/GF and U/W patterns into a Δ2… | ||
| Automata-Driven Partial Order Reduction and Guided Search for LTL Model Checking | Peter Gjol Jensen, Jiri Srba, Nikolaj Jensen Ulrik, Simon Mejlby Virenfeldt | 29m |
Paper implements automata-driven stubborn sets and a heuristically guided search inside TAPAAL 3.9, reusing progression formulas from the Büchi automaton to… | ||
| Scaling Up Livelock Verification for Network-on-Chip Routing Algorithms | Landon Taylor, Zhen Zhang | 26m |
Refutation-based simulation scales verification from refutation-based simulation on small meshes to an IVy-checked model up to 15x15, implemented with a C++… | ||
| Bisimulations for Neural Network Reduction | Pavithra Prabhakar | 28m |
Defines a neural-network bisimulation based on a pre-sum operator that merges nodes within layers and yields a quotient network with identical input–output… | ||
| High Assurance Software for Financial Regulation and Business Platforms | Stephen Goldbaum, Attila Mihaly, Tosha Ellison, Earl Barr, Mark Marron | 31m |
An open stack called Morphir compiles Elm and Legend into a pure, loop‑free MorphirIR that maps one‑to‑one to SMT theories and is checked with SMT/Z3 encodings… | ||
| Loop Verification with Invariants and Contracts | Gidon Ernst | 30m |
Loop contracts pair an invariant with a relational summary and claim strictly more expressiveness than invariants alone while admitting a constructive… | ||
| Making PROGRESS in Property Directed Reachability | Tobias Seufert, Christoph Scholl, Arun Chandrasekharan, Sven Reimer, Tobias Welp | 28m |
Implements Proof-Guided Restriction Skipping (PROGRESS) on top of PDR/IC3 to run model checking under arbitrary restrictions (fixing inputs/state bits to… | ||
| Gradient-Descent for Randomized Controllers under Partial Observability | Jip Spel, Linus Heck, Sebastian Junges, Joshua Moerman, Joost-Pieter Katoen | 28m |
Transforms partially observable controllers into a parametric Markov chain and computes exact derivatives by building a derived weighted automaton so gradients… | ||
| Satisfiability and Synthesis Modulo Oracles | Elizabeth Polgreen, Andrew Reynolds, Sanjit A. Seshia | 34m |
Defines a formal SMTO/SyMO framework that plugs executable black‑box oracles into SMT/synthesis via assumption generator and constraint generator interfaces… | ||
| Out of Control: Reducing Probabilistic Models by Control-State Elimination | Tobias Winkler, Johannes Lehmann, Joost-Pieter Katoen | 23m |
Title:[VMCAI'22] Out of Control: Reducing Probabilistic Models by Control-State Elimination
Authors:Tobias Winkler, Johannes Lehmann, Joost-Pieter… | ||
| STAMINA 2.0: Improving Scalability of Infinite-StateStochastic Model Checking | Riley Roberts, Thakur Neupane, Lukas Buecherl, Chris Myers, Zhen Zhang | 26m |
STAMINA 2.0 implements a combined CTMC transient analysis with PRISM to produce min/max probability bounds in one pass, replaces predecessor-sum reachability… | ||
| EPMC Gets Knowledge in Multi-Agent Systems | Chen Fu, Ernst Moritz Hahn, Yong Li, Sven Schewe, Meng Sun, Andrea Turrini, Lijun Zhang | 22m |
EPMC is a small Java core plus plugins probabilistic model checker that the authors extend to EPMC-petl to handle probabilistic epistemic temporal logic on… | ||
| Simplifying Concurrent Programming via Synchronization Synthesis | Isil Dillig | 01h 08m |
Given an implicit-monitor spec using conditional critical regions, the system synthesizes concrete locks and condition-variable operations by reducing… | ||
| Fast Three-Valued Abstract Bit-Vector Arithmetic | Jan Onderka, Stefan Ratschan | 30m |
The work gives polynomial-time algorithms that compute the best three-valued abstract result for bit-vector addition and multiplication: addition in linear… | ||
| Mixed Semantics Guided Layered Bounded Reachability Analysis of Compositional L | Yuming Wu, Lei Bu, Jiawan Wang, Xinyue Ren, Wen Xiong, Xuandong Li | 33m |
Enumerates candidate step semantics then shallow semantics paths: the discrete layer generates step-based compositional paths, the continuous layer generalizes… | ||
| Stateful Dynamic Partial Order Reduction for Model Checking Event-Driven Applic | Rahmadi Trimananda, Weiyu Luo, Brian Demsky, Harry Xu | 30m |
Presents a new stateful DPOR algorithm that is sound for non-terminating, event-driven programs by adding a novel termination criterion, computing conflicts… | ||
| nothing matches | ||