Monotone Procedure Summarization via Vector Addition Systems and Inductive Potentials
summary
Computes the best VASR reflection that linearly simulates the program, then exactly solves context-free-language reachability over that VASR to get procedure summaries; synthesizes linear bounds on recursive call counts via inductive potentials (encoded as a polyhedron) and applies them to strengthen the summary; guarantees monotone summarization (refinements never weaken summaries); implements the approach in LIP, evaluates on a new RecSupreme benchmark, and matches or outperforms some model checkers on recursive tasks.
AI-written summary · about
chapters (13)
- 0:00Monotone procedure summarization intro
- 1:46Limitations of current summarizers
- 3:56Goal of predictable summarization
- 4:59Verification with memory bounds
- 6:23Computing best VASER abstractions
- 8:31VASER reflection and simulation
- 10:42CFL reachability in VASER
- 12:08Lossy VASER for inequalities
- 12:53Refining summaries with potentials
- 15:01Evaluating on SV-COMP
- 16:30Combining monotone summarizers
- 17:12Summary of contributions
- 17:33Q&A
related talks
15mProducts of Recursive Programs for Hypersafety Verification
27mParameterized Infinite-State Reactive Synthesis
46mPropagators
19mSolving Infinite-State Games via Acceleration
29mRewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata
16mCyclic Message Histories for Automated Safety Verification of Distributed Algorithms
19mMostly Automated Verification of Liveness Properties for Distributed Protocols w...
31mCompositional Verification of Stigmergic Collective Systems