Verifying Safety of Functional Programs with Rosette/Unbound
Abstract
The goal of unbounded program verification is to discover an inductive invariant that safely over-approximates all possible program behaviors. Functional languages featuring higher order and recursive functions become more popular due to the domain-specific needs of big data analytics, web, and security. We present Rosette/Unbound, the first program verifier for Racket exploiting the automated constrained Horn solver on its backend. One of the key features of Rosette/Unbound is the ability to synchronize recursive computations over the same inputs allowing to verify programs that iterate over unbounded data streams multiple times. Rosette/Unbound is successfully evaluated on a set of non-trivial recursive and higher order functional programs.
Cite
@article{arxiv.1704.04558,
title = {Verifying Safety of Functional Programs with Rosette/Unbound},
author = {Dmitry Mordvinov and Grigory Fedyukovich},
journal= {arXiv preprint arXiv:1704.04558},
year = {2017}
}