Fri 12 Jan 2018 13:30 - 13:52 at Bunker Hill - Program Analysis II Chair(s): Isil Dillig

We introduce Refinement Reflection, a new framework for building SMT-based deductive verifiers. The key idea is to reflect the code implementing a user-defined function into the function’s (output) refinement type. As a consequence, at uses of the function, the function definition is instantiated in a precise fashion that permits decidable verification. We show how reflection allows the user to write equational proofs of programs just by writing other programs e.g., using pattern-matching and recursion to perform case-splitting and induction. Thus, via, the propositions-as-types principle we show that reflection permits the specification of arbitrary functional correctness properties. While equational proofs are easy, writing them out can be exhausting. We introduce a proof-search 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 to build the first library that actually verifies assumptions about associativity and ordering that are crucial for safe deterministic parallelism.

Fri 12 Jan

13:30 - 15:20: Research Papers - Program Analysis II at Bunker Hill
Chair(s): Isil DilligUT Austin
POPL-2018-papers13:30 - 13:40
Benjamin DelawarePurdue University
POPL-2018-papers13:30 - 13:52
Niki VazouUniversity of Maryland, Anish TondwalkarUCSD, Vikraman Choudhury, Ryan ScottIndiana University, Ryan R. NewtonIndiana University, Philip WadlerUniversity of Edinburgh, UK, Ranjit JhalaUniversity of California, San Diego
POPL-2018-papers14:05 - 14:30
Zachary KincaidPrinceton University, John CyphertUniversity of Wisconsin - Madison, Jason BreckUniversity of Wisconsin - Madison, Thomas RepsUniversity of Wisconsin - Madison and GrammaTech, Inc.
POPL-2018-papers14:30 - 14:55
POPL-2018-papers14:55 - 15:20
Yuepeng WangUniversity of Texas at Austin, Isil DilligUT Austin, Shuvendu K. LahiriMicrosoft Research, William CookUniversity of Texas at Austin