Rosette/Unbound函数式程序的安全性
Verifying Safety of Functional Programs with Rosette/Unbound
摘要：
无界程序验证的目标是发现一个归纳不变量，安全地过近似所有可能的程序行为。由于大数据分析、Web和安全的特定领域需求，具有高阶和递归函数的函数式语言变得更加流行。我们提出了玫瑰花/Unbound，第一个程序验证球拍利用自动约束霍恩求解器的后端。Rosette/Unbound的一个关键特性是能够在相同的输入上同步递归计算，从而允许验证多次在无界数据流上进行递归计算的程序。Rosette/Unbound在一组非平凡的递归和高阶函数程序上成功地进行了评估。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
