Simple and Efficient Computation of Minimal Weak Control Closure
summary
Method computes minimal weak control closure by identifying V-paths and locating “weakly deciding vertices” via a backward traversal that builds an over-approximation W then verification phase, discards unreachable nodes, and returns V∪W. Claim: worst-case complexity is quadratic worst-case versus prior cubic/quartic methods. Implementation in Clang/LLVM implementation and experiments on SPEC CPU2017 (2,081 KLOC) show speedups from 2.9× to 23.8× (average ~10.6×; VM runs ~5.4×). Works for intra-procedural graphs including nonterminating exits.
AI-written summary · about
chapters (10)
- 0:00Intro
- 0:17Control Dependency Relation
- 1:21From V-paths to Weak Control Closure
- 3:30Theoretical Complexity
- 4:12Applicability - Scope of Programs
- 6:26Step 1: Computing Weakly Deciding Vertices
- 12:02Step 2: Verification of Weakly Deciding Vertices
- 15:35WCC computation (Final Phase)
- 17:49Comparing Execution Times
- 18:28Conclusion and Future Work
related talks
17mExploiting the Sparseness of Control-Flow and Call Graphs for Efficient and On-...
21mMutual Refinements of Context-Free Language Reachability
22mExecution Time Program Verification With Tight Bounds
01h 09mPlenary: Neighborhoods Banding Together: Reasoning Globally about Programs
18mWP-Preserving Compilation -- Preserving Weakest Preconditions For End-to-End Verification
58mA New Perspective on Commutativity in Verification
18mOn the Verification of a Subgraph Construction Algorithm
31mTermination in Concurrency, Revisited