Scalability and Precision by Combining Expressive Type Systems and Deductive Verification
summary
Implementation builds a Property Checker and a JML translator that converts unproven type checks into assertions for KeY/OpenJML and proven ones into assumptions. Applied to Daikon snippets it discharges real Checker Framework false positives. In a case study 117 JML obligations reduce to 27 after the checker discharges 90, dropping KeY time from ~500s to 311s plus 8s for the checker and cutting extra JML clauses from 55 to 50.
AI-written summary · about
chapters (10)
- 0:00Intro
- 0:21Motivation
- 2:55Core idea
- 4:48What are Property Types?
- 5:28Property Type Hierarchies
- 7:09JML Translation
- 8:15Deductive verification
- 8:49Evaluation Correcting false positives in Daikon
- 9:38Evaluation: Case Study
- 12:01Conclusion
related talks
01h 02mLanguage Design meets Verifying Compilers
21mMechanised Hypersafety Proofs about Structured Data
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
21mPractical Type Inference with Levels
24mSet-Theoretic Type Checking of Beginner Erlang Code: A Retrospective Study
22mVerification Modulo Tested Library Contracts
28mGradual Verification: Assuring Software Incrementally
24mProving False in Object Oriented Verification Programs by Exploiting Non-Termination