SOAP - Keynote: Formal Reasoning and the Hacker Way
summary
A compositional static analyzer called Infer is wired into CI to run on diffs rather than nightly batches, and this deployment change raises developer fix rate from near 0% in batch to about 70% fix rate at code review. A separate concurrent analysis built with ideas from separation logic ships as a pragmatic checker and finds over 2.5k races in a year in production (no false negatives observed there), trading theoretical soundness for usable, fast results.
AI-written summary · about
chapters (12)
- 0:00Start
- 0:44The Hacker Way
- 9:00The Frame Rule
- 14:29Hacking a Program Analyzer
- 17:47Dynamic Analysis
- 18:24Concurrent Separation Logic
- 19:10The Engineering Context
- 24:19Inter Procedural Concurrency Analysis
- 35:57The True Positives Theorem
- 36:25The Deep Ownership Assumption
- 44:11Proof Rules for Reiteration
- 51:09State of Program Analysis
related talks
01h 00mCurrent State of the Industrial-Strength Infer Static Analysis Platform
50mExpanding the scope of refactoring to fix Java security problems
23mStopping vulnerabilities at the source
42mContemporary Automatic Program Analysis
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
59mUnder-approximation for Scalable Bug Detection
46mRugged Software Engineering
44mWe Hate Code: The !Joy of Maintaining Dead Code