使用Stellens"atze的模板化程序合成
摘要：基于模板的综合，也被称为草图，是一种定位的程序综合方法，程序员不仅提供规范，还提供了程序的高级“草图”。草图基本上是一个部分程序，用于模拟程序员的一般直觉，同时将低级细节作为未实现的“空洞”。综合引擎的作用是填补这些空洞，以使完成的程序满足所需的规范。在这项工作中，我们专注于基于模板的多项式命令式程序与实数变量的综合，即在赋值、条件和保护中出现的所有表达式都是关于程序变量的多项式的命令式程序。虽然这个问题可以通过将其归约到实数的一阶理论来以一种准确和完整的方式解决，但结果公式将包含量化器交替，并且对于现代SMT求解器来说非常困难，即使考虑只有几行代码的小型程序也是如此。此外，量化器消除的经典算法因其扩展性不佳且不适用于该用例而臭名昭著。 相比之下，我们的主要贡献是一种算法，基于多面体和实代数几何学中的几个公认定理，即Putinar的正定定理、实零点定理、Handelman的定理和Farkas的引理，避开了量化器消除的困难，直接将问题归约为二次规划（QP）。或者，我们可以将我们的算法视为消除综合问题中出现的特定公式中的量化器的有效方法。然后，可以通过SMT求解器轻松处理得到的QP实例。值得注意的是，我们对QP的归约是准确和半完整的，即如果模板中使用高次多项式，则它是完整的...
作者：Amir Kafshdar Goharshady, S. Hitarth, Fatemeh Mohammadi, Harshit J Motwani
论文ID：2209.03602
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-09-09