Projects per year
Abstract / Description of output
We introduce Refinement Reflection, a new framework for building SMTbased deductive verifiers. The key idea is to reflect the code implementing a userdefined function into the function's (output) refinement type. As a consequence, at uses of the function, the function definition is instantiated in the SMT logic in a precise fashion that permits decidable verification. Reflection allows the user to write equational proofs of programs just by writing other programs using patternmatching and recursion to perform casesplitting and induction. Thus, via the propositionsastypes principle, we show that reflection permits the specification of arbitrary functional correctness properties. Finally, we introduce a proofsearch algorithm called Proof by Logical Evaluation that uses techniques from model checking and abstract interpretation, to completely automate equational reasoning. We have implemented reflection in Liquid Haskell and used it to verify that the widely used instances of the Monoid, Applicative, Functor, and Monad typeclasses actually satisfy key algebraic laws required to make the clients safe, and have used reflection to build the first library that actually verifies assumptions about associativity and ordering that are crucial for safe deterministic parallelism.
Original language  English 

Number of pages  31 
Journal  Proceedings of the ACM on Programming Languages 
Volume  2 
DOIs  
Publication status  Published  27 Dec 2017 
Fingerprint
Dive into the research topics of 'Refinement Reflection: Complete Verification with SMT'. Together they form a unique fingerprint.Projects
 1 Finished

From Data Types to Session Types  A Basis for Concurrency and Distribution
20/05/13 → 19/11/20
Project: Research