VMCAI 2023
2023-01-15..2023-01-17
Boston, United States
VMCAI ·
[VMCAI 2022, VMCAI 2023, VMCAI 2024, VMCAI 2025, VMCAI 2026]
| title | author | length |
|---|---|---|
| Distributing and Parallelizing Non-canonical Loops | Clément Aubert, Thomas Rubiano, Neea Rusch, Thomas Seiller | 27m |
An algorithm that builds a data flow graph, collapses it into a condensation graph, computes a proper saturated covering and emits loop-fissioned code, proven… | ||
| Efficient Interprocedural Data-Flow Analysis using Treedepth and Treewidth | Amir Kafshdar Goharshady, Ahmed Khaled Zaher | 30m |
Claims a concrete IFDS solver that exploits treedepth of the call graph and treewidth of control-flow graphs, constructs an exploded code graph, and achieves… | ||
| Result Invalidation for Incremental Modular Analyses | Jens Van der Plas, Quentin Stiévenart, Coen De Roover | 28m |
Introduces three concrete invalidation strategies—component invalidation, dependency invalidation, and provenance-based write invalidation—and interleaves… | ||
| Towards a Theoretical Understanding of Property-Directed Reachability | Sharon Shoham | 59m |
Shows that the SAT queries used by property‑directed reachability are strictly stronger than plain inductiveness checks, proving IC3 cannot be implemented in… | ||
| Symbolic Abstract Heaps for Polymorphic Information-flow Guard Inference | Nicolas Berthier, Narges Khakpour | 34m |
Presents a symbolic store-less heap abstraction parameterized by relations (dumb, shallow, deep) and uses co-reachability on a deterministic symbolic… | ||
| What Can Program Analysis Say About Data Bias? | Aws Albarghouthi | 59m |
Proposes a method that uses abstract interpretation to symbolically represent all datasets within a bias model (e.g., up to n label flips) and lift core… | ||
| Bayesian parameter estimation with guarantees via interval analysis and simulat... | Luisa Collodi | 26m |
Method computes provable Bayesian posterior estimates for models y = f(θ) + h(ψ) (covers noisy ODE parameters and neural-network f) by combining P-boxes… | ||
| Solving Constrained Horn Clauses over Algebraic Data Types | Lucas Zavalia, Lidiia Chernigovskaia, Grigory Fedyukovich | 23m |
Implements a solver called AdtChc that synthesizes recursive functions from CHCs over algebraic data types using equality propagation and a new-fun transform… | ||
| Satisfiability Modulo Custom Theories in Z3 (Tool Paper) | Nikolaj Bjørner, Clemens Eisenhofer, Laura Kovács | 32m |
Z3 adds user-propagators: an API to register ground terms and attach callbacks (fixed, equality, instantiate, final) written in C++/Python that can emit… | ||
| Differential Verification of Deep Neural Networks | Chao Wang | 59m |
[VMCAI'23] Differential Verification of Deep Neural Networks
Chao Wang
Deep neural networks have become an integral component of many systems for which… | ||
| ARENA: Enhancing Abstract Refinement for Neural Network Verification | Yuyi Zhong, Quang-Trung Ta, Siau-Cheng Khoo | 31m |
ARENA implements an abstract-refinement verifier that uses the double description method over convex polytopes to turn disjunctions into LP-friendly… | ||
| Maximal Robust Neural Network Specifications via Oracle-guided Numerical Optimi... | Anan Kabaha, Dana Drachsler Cohen | 12m |
MaRVeL computes maximal non-uniform robust specifications that explicitly maximize a chosen norm by coupling a numerical optimizer with a non-differentiable… | ||
| SMT-Based Modeling and Verification of Spiking Neural Networks: A Case Study | Ansuman Banerjee, Soham Banerjee, Sumana Ghosh, Swarup Kumar Mohalik | 15m |
SMT encoding models LIF neurons with Linear Real Arithmetic and runs on Z3 plus SNN Torch to verify properties and adversarial robustness on IRIS and MNIST… | ||
| A generic framework to coarse-grain stochastic reaction networks by Abstract In... | Jerome Feret, Albin Salazar | 30m |
A reproducible method converts reaction networks into coarse-grained discrete models using Abstract Interpretation, an interval lattice and a discrete-time… | ||
| Sound Symbolic Execution via Abstract Interpretation and its Application to Sec... | Tamara Rezk, Xavier Rival, Ignacio Tiraboschi | 31m |
Combines symbolic execution with abstract interpretation to get sound proofs plus bounded counterexample pairs, claiming a formally proven analyzer called… | ||
| Verifying, Inferring and Exploiting Code Commutativity | Eric Koskinen | 01h 16m |
[VMCAI'23] Verifying, Inferring and Exploiting Code Commutativity
Eric Koskinen
Algebraic commutativity has long been used as an effective abstraction… | ||
| Compositional Verification of Stigmergic Collective Systems | Luca Di Stefano, Frederic Lang | 31m |
Claim: compositional verification plus a lightweight static value analysis tames state-space explosion for stigmergic agent systems. Implementation encodes… | ||
| Synthesizing History and Prophecy Variables for Symbolic Model Checking | Cole Vick, Kenneth L. McMillan | 32m |
Presents an automated CEGAR pipeline that introduces prophecy and history variables to remove universal quantifiers over arrays, using counterexample-guided… | ||
| A Pragmatic Approach to Stateful Partial Order Reduction | Berk Cirisci, Constantin Enea, Azadeh Farzan, Suha Orhun Mutluergil | 16m |
Proposes stateful POR variants: a cheap static safe-set pass plus two dynamic source-set trackers (eager and lazy) implemented in Java Pathfinder. Benchmarks… | ||
| StaticPersist : Compiler Support for PMEM Programming | Sorav Bansal | 15m |
StaticPersist implements a compile-time interprocedural points-to analysis on LLVM IR that statically marks allocations as persistent or volatile and rewrites… | ||
| nothing matches | ||