The Never-Ending Trace: An Under-Approximate Approach to Divergence Bug...
summary
Introduces a forward under-approximating triple that expresses “for every prestate there exists an execution that diverges,” with a divergent variant that detects infinite loops from loops, recursive calls and unstructured goto-cycles. Uses a conditional triple parameterized by a history G of (label, assertion); a goto-step rule appends unseen (label,assertion) to G and a goto-rec rule concludes divergence when an identical (label,assertion) reappears. Claims functional compositionality for functions, under-approximation (all reported bugs are reachable), completeness for while-only fragments and unknown completeness for the recursion/goto extension.
AI-written summary · about
chapters (17)
- 0:00Introduction
- 1:05Limitations of total correctness
- 2:50Backward under-approximation
- 4:14Programs as go-to soups
- 5:37Divergence in go-to programs
- 7:02Divergence with conditional triples
- 9:09Proof on go-to example
- 10:56Q&A
- 12:01Q&A
- 12:42Q&A
- 13:45Q&A
- 16:11Q&A
- 16:54Q&A
- 17:15Q&A
- 18:21Q&A
- 18:42Q&A
- 19:03Closing
related talks
19mNon-Termination Proving at Scale
21mAbstract Debuggers: Exploring Program Behaviors Using Static Analysis Results
59mUnder-approximation for Scalable Bug Detection
32mGenerative Testing: Properties, State and Beyond
20mMisconceptions About Loops in C
26mThe missing piece of testing
47mDeterministically Debugging Go Programs
26mCatching Every Bug: Integrating Testing, Observability, Determinism & then what?