2 papers
cs.PL2021
Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types (Extended Version)
Anish Tondwalkar, Matthew Kolosick, Ranjit Jhala
Refinement types decorate types with assertions that enable automatic verification. Like assertions, refinements are limited to binders that are in scope, and hence, cannot express…
cs.PL2017
Refinement Reflection: Complete Verification with SMT
Niki Vazou, Anish Tondwalkar, Vikraman Choudhury +4
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 fu…