Verifying Safety of Functional Programs with Rosette/Unbound
This addresses the need for reliable verification in functional programming, which is increasingly used in domains like big data and security, though it appears incremental as it builds on existing solver techniques.
The authors tackled the problem of verifying safety properties of functional programs with higher-order and recursive features by developing Rosette/Unbound, a verifier for Racket that uses an automated constrained Horn solver, and successfully evaluated it on non-trivial programs.
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.