True
is a bad argument10
is a good argument0
average
take
fib
fib
is an uninterpreted function
Liquid Haskell:
Verification of Haskell Code
github @ https://github.com/ucsd-progsys/liquidhaskell
book @ http://www.refinement-types.org
online demo @ http://goto.ucsd.edu/liquidhaskell
cabal install liquidhaskell
DONE
Coming up
Diverse Code Bases
20KLoc
Memory Safety, Termination, Functional Correctness, Program Equivalence
Specifications: 1 / 10 LOC
Library | LOC | Specs | Time |
---|---|---|---|
XMonad.StackSet |
256 | 74 | 27s |
Data.List |
814 | 46 | 26s |
Data.Set.Splay |
149 | 27 | 27s |
Data.Vector.Algorithms |
1219 | 76 | 89s |
HsColour |
1047 | 19 | 196s |
Data.Map.Base |
1396 | 125 | 174s |
Data.Text |
3128 | 305 | 499s |
Data.Bytestring |
3505 | 307 | 294s |
Total | 11512 | 977 | 1336s |
Liquid Types: Automated Verification via SMT
Properties: | Predicates + Types |
Proofs: | SMT Solvers + Subtyping |