Semantic-Type-Guided Bug Finding
summary
Introduces a semantic-type refuter that is co-recursively enumerable and proves soundness and completeness against a semantic model; implements the checker and generator approach in an OCaml implementation and encodes checks as error-reachability solved by a concolic validator. Demonstrates detection of real bugs (including an AVL tree rebalance counterexample), outperforms a 2015 SCV artifact on most benchmarks, and times out on some correct recursive programs so it is best used as a complement to conventional type systems.
AI-written summary · about
chapters (8)
- 0:00Semantic-type-guided bug finding
- 3:54Language and type checking
- 7:01Generator and checker functions
- 9:49Dependent function types
- 11:33Implementation and example
- 13:43AVL tree performance
- 14:46Limitations and future work
- 15:33Q&A
related talks
16mSoftware Model Checking via Summary-Guided Search
17mA HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite(…)
13mA Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs
24mSet-Theoretic Type Checking of Beginner Erlang Code: A Retrospective Study
22mFrom FP to OOP and Back, Consistently
40mFinding bugs without running or even looking at code
24mSymbiotic: finding bugs in C programs
14mScalability and Precision by Combining Expressive Type Systems and Deductive Verification