Algorithmic Verification
11: {v : (IO ()) | v == Main.main}main = [Char] -> (IO ())putStrLn {v : [Char] | len v >= 0}"Easter Egg: to force Makefile"
Goal
Automatically Proving Properties of Programs
Algorithmic Verification
A Classic Example
Verify: indices i, min are within bounds of arr
A Classic Example
Easy, use Program Logic + Analysis
Program Logic
| Specification | Predicates eg. invariants, pre-/post-conditions |
| Verification | Conditions checked by SMT solver |
Program Logic
| Specification | Predicates eg. invariants, pre-/post-conditions |
| Verification | Conditions checked by SMT solver |
No invariants? Inference via Analysis...
Program Analysis
Invariants are Fixpoints of Reachable States
Computable via Dataflow Analysis or Abstract Interpretation
Logic + Analysis
| Specification | Predicates, eg. invariants, pre-/post-conditions |
| Verification | Conditions checked by SMT solver |
| Inference | Fixpoint over abstract domain |
But ... limited to "classical" programs!
"Classical" vs. "Modern" Programs
"Classical" Programs
Imperative
Assignments, Branches, LoopsFirst-Order Functions
RecursionObjects
Classes, Inheritance*"Modern" Programs
Containers
Arrays, Lists, HashMaps,...
Polymorphism
Generics, Typeclasses...Higher Order Functions
Callbacks, map, reduce, filter,...A "Modern" Example
Verify indices i, min are within bounds of arr
A "Modern" Example
Pose vexing challenges for Logic + Analysis
Logic + Analysis Challenges
- How to analyze unbounded contents of
arr? - How to summarize
reduceindependent ofcallback? - How to precisely reuse summary at each context ?
Logic + Analysis + Types
Logic + Analysis + Types
Refinement Types
Use Types to lift Logic + Analysis to Modern Programs
| Specification | Types + Predicates | ||||
| Verification | Subtyping + Verification Conditions | ||||
| Inference | Type Inference + Abstract Interpretation |
Refinement Types
Plan