On-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
summary
An analyzer implementation (CiaoPP) performs top‑down, context‑ and path‑sensitive abstract interpretation with incremental, modular fixpoint reuse via call/answer tables and call-answer memoization and dependency arcs so edits reanalyze only affected modules, often giving order‑of‑magnitude speedups. Assertions get statically checked, failing proofs become inserted runtime tests, and analyses plug different domains (types, aliasing, cost, termination). The system translates other languages to constraint Horn clauses, runs the whole toolchain compiled to wasm browser embedding, and powers interactive IDE feedback and in‑document tutorials.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 2:40On-the-fly verification goals
- 9:06Analyzer algorithm and abstract interpretation
- 16:31Incremental analysis with snapshots
- 21:29Verification in IDEs
- 23:37Live demo: CHR Pro verification
- 41:40Advanced features and assertions
- 48:06Browser-based verification
- 54:08Summary and future directions
- 55:15Q&A
related talks
21mLive Verification in an Interactive Proof Assistant
56mMy Journey to the Dark Side: Under-Approximation, Incorrectness, Proof
21mAbstract Debuggers: Exploring Program Behaviors Using Static Analysis Results
50mState of the Infer Platform
28mGradual Verification: Assuring Software Incrementally
22mFormal Runtime Error Detection During Development in the Automotive Industry
01h 00mCurrent State of the Industrial-Strength Infer Static Analysis Platform
25mIncremental Type-Checking for Free: Using Scope Graphs to Derive Incremental Type-Checkers