Termination Analysis for Evolving Programs: An Incremental Approach by Reusing Certified Modules
summary
Presents an incremental termination checker that reuses certified modules extracted from prior runs, implemented on top of UAutomizer and tested on 276 Codeforces run sets (611 revisions). Reuse extracts predicates and Hoare triples, drops ones invalidated by edits, adds triples for changed blocks, and reconstructs certified modules over the new alphabet. Results show average speedup 3.08×, average 5.68 modules reused, a case of 25/26 modules reused yielding 13×, and up to 5× on 60% diffs; Frama‑C distinguishes loop‑relevant changes.
AI-written summary · about
chapters (11)
- 0:00Intro
- 0:14Termination
- 3:23Certified Modules
- 4:34A New Version
- 6:26Module as Set of Hoare Triples
- 8:59Reuse Procedure
- 11:15Implementation / Evaluation
- 12:42Degree of Program Changes
- 13:54A Heavily-Changed Example
- 14:28Loop-Relevant Changes
- 15:20Conclusion
related talks
15mIncremental Certified Programming
26mTowards Efficient Model Comparison Using Automated Program Rewriting
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
30mModularity, Code Specialization, and Zero-Cost Abstractions for Program Verifica...
22mFormal Runtime Error Detection During Development in the Automotive Industry
28mGradual Verification: Assuring Software Incrementally
50mGuide Refactorings With Behavioral Code Analysis
01h 23mMidnote: Why Cpp Loops End