LiquidHaskell

Refinement Types via SMT and Predicate Abstraction