Refinement reflection

complete verification with SMT

conference
Authors
Affiliations

Niki Vazou

University of Maryland, USA

Anish Tondwalkar

University of California at San Diego, USA

Vikraman Choudhury

Indiana University, USA

Ryan G. Scott

Indiana University, USA

Ryan R. Newton

Indiana University, USA

Philip Wadler

University of Edinburgh, UK / Input Output HK, UK

Ranjit Jhala

University of California at San Diego, USA

Published

December 27, 2017

Doi

10.1145/3158141

Abstract

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 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 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. Finally, 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 have used reflection to build the first library that actually verifies assumptions about associativity and ordering that are crucial for safe deterministic parallelism.

Back to top

Citation

BibTeX citation:
@inproceedings{vazou2017,
  author = {Vazou, Niki and Tondwalkar, Anish and Choudhury, Vikraman
    and G. Scott, Ryan and R. Newton, Ryan and Wadler, Philip and Jhala,
    Ranjit},
  title = {Refinement Reflection},
  booktitle = {Proceedings of the ACM on Programming Languages},
  date = {2017},
  url = {https://doi.org/10.1145/3158141},
  doi = {10.1145/3158141},
  langid = {en},
  abstract = {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 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 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.
    Finally, 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 have used
    reflection to build the first library that actually verifies
    assumptions about associativity and ordering that are crucial for
    safe deterministic parallelism.}
}
For attribution, please cite this work as:
Vazou, Niki, Anish Tondwalkar, Vikraman Choudhury, et al. 2017. “Refinement Reflection.” Proceedings of the ACM on Programming Languages, accepted. https://doi.org/10.1145/3158141.