DynamiTe: Dynamic Termination and Non-termination Proofs
summary
DynamiTe is a Python tool that instruments loops with vtrace instrumentation and iteration counters, learns linear ranking functions from concrete terminating traces, and searches for recurrent sets from possibly non-terminating traces. It hands off candidates to external safety provers for validation and refines using counterexample-driven inputs. Evaluation: on 67 non-linear programs DynamiTe infers ranking functions for 37 but only 5 validate; it proves non-termination for 37 programs and sometimes succeeds where Ultimate Automizer fails. Code: github.com/letonchanh/dynamite.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:33Motivating Examples
- 3:03Background: Dynamic Analysis
- 4:05Dynamic Termination and Non-termination Proofs: Overview
- 4:30Program Instrumentation, Trace Collection and Classification
- 5:31Dynamic Termination Proof
- 8:17Dynamic Non termination Proof
- 10:10An Integrated Algorithm
- 11:09Implementation and Evaluation
- 11:44Experimental Results
- 12:33Conclusion
related talks
24mProving False in Object Oriented Verification Programs by Exploiting Non-Termination
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
15mDynaplex: Analyzing Program Complexity using Dynamically Inferred Recurrence Relations
15mOn the Impact of Formal Verification on Software Development
01h 02mLanguage Design meets Verifying Compilers
01h 23mMidnote: Why Cpp Loops End
14mScalability and Precision by Combining Expressive Type Systems and Deductive Verification
20mFormal framework for reasoning about the precision of dynamic analysis