Non-Termination Proving at Scale
summary
Claims a sound and complete under-approximate logic called UNTerSL that composes incorrectness/divergence reasoning with separation logic and bi-abduction to prove non-termination in heap code, and an automated prover Pulse∞ built on Infer/Pulse that scales to real projects. It analyzes ~800,000 lines in 90 seconds, finds several previously unknown non-termination bugs in OpenSSL, libxml2, libxpm and CryptoPP (e.g. an IO-driven loop that never breaks, a retry-without-bound malloc loop), and reports fixes.
AI-written summary · about
chapters (10)
- 0:00Non-termination proving intro
- 1:27Termination bugs importance
- 2:51Incorrectness logic foundations
- 3:54Forward and backward under-approximation
- 6:26Non-termination as incorrectness
- 7:30Hunter logic for divergence
- 9:16Lasso properties in divergence
- 10:38Infer framework implementation
- 11:22Real-world divergence bugs
- 12:47Q&A
related talks
59mUnder-approximation for Scalable Bug Detection
40mBridging the Gap For Security Analysis In Infer
31mA Comparison of Program Logics for (In)Correctness
42mQuantum program analysis: Verification and Testing
19mThe Never-Ending Trace: An Under-Approximate Approach to Divergence Bug...
18mType-Based Incorrectness Reasoning
18mPreview: Verification (Correctness)
56mMy Journey to the Dark Side: Under-Approximation, Incorrectness, Proof