论文标题
UCLID5中的合成
Synthesis in Uclid5
论文作者
论文摘要
我们描述了程序合成纳入UCLID5的集成，UCLID5是一种形式的建模和验证工具。据我们所知，新版本的UCLID5是支持程序合成的唯一工具，该工具具有有限的模型检查，k诱导，顺序程序验证和超级验证验证。我们使用集成来生成25种程序合成基准，并具有简单的，已知的解决方案，这些解决方案无法触及当前的合成引擎，并且我们将基准释放到社区。
We describe an integration of program synthesis into Uclid5, a formal modelling and verification tool. To the best of our knowledge, the new version of Uclid5 is the only tool that supports program synthesis with bounded model checking, k-induction, sequential program verification, and hyperproperty verification. We use the integration to generate 25 program synthesis benchmarks with simple, known solutions that are out of reach of current synthesis engines, and we release the benchmarks to the community.
