Refinement Reflection:
Complete Verification with SMT

Niki Vazou
(University of Maryland)

Type-Theory-based theorem provers

  • Type level computation to reason about program properties.

  • Supply lemmata or rewrite hints to discharge proofs, ...

  • ... even in decidable logics.

SMT-based verifiers

  • Automate the verification of programs over decidable theories.

  • Encode user-defined functions with universally-quantified axioms, ...

  • ... using incomplete (i.e., unpredictable) heuristics for instantiation.

Predictable & SMT-automated Verification

GOAL: Alternative representation of user-defined functions ...

... for SMT-decidable (i.e., unpredictable) verification.

Refinement Reflection

Reflect function definition into its result refined type.


Value level function application is also ...

... "SMT" predictable function instantiation.


How far can we go?



  • Refinement Reflection and Proof by Logical Evaluation combined ...

  • ... allow for complete verification with SMT-automation, but

  • ... don't allow for user interaction,

  • ... don't allow for proof certificates.

Thank you!

Refinement Reflection: Complete Verification with SMT

to appear in POPL 2018

  • by Niki Vazou, Anish Tondwalker, Vikraman Choudhoury,
  • Ryan Scott, Ryan Newton, Philip Wadler, and Ranjit Jhala