Recent years have seen tremendous growth in the amount of verified software. Proofs for complex properties can now be achieved using higher-order theories and calculi. Complex properties lead to an ever-growing number of definitions and associated lemmas, which constitute an integral part of proof construction. Following this -- whether automatic or semi-automatic -- methods for computer-aided lemma discovery have emerged. In this work, we introduce a new symbolic technique for bottom-up lemma discovery, that is, the generation of a library of lemmas from a base set of inductive data types and recursive definitions. This is known as the theory exploration problem, and so far, solutions have been proposed based either on counter-example generation or the more prevalent random testing combined with first-order solvers. Our new approach, being purely deductive, eliminates the need for random testing as a filtering phase and for SMT solvers. Therefore it is amenable compositional reasoning and for the treatment of user-defined higher-order functions. Our implementation has shown to find more lemmas than prior art, while avoiding redundancy.
翻译：近些年来,经过核实的软件数量有了巨大的增长。现在,可以用更高层次的理论和计算法来证明复杂的特性。复杂的特性导致越来越多的定义和相关的 Lemmas, 它们是证据构建的一个组成部分。 之后, 无论是自动还是半自动的, 计算机辅助的 Lemma 发现方法已经出现。 在这项工作中, 我们为自下而上的 Lemma 发现引入一种新的象征性技术, 即从一组基本的感应数据类型和循环定义中生成一个利玛书库。 这被称为理论探索问题。 到目前为止, 已经根据反例生成或与一级解答器相结合的更为普遍的随机测试提出了解决方案。 我们的新方法是纯粹的推理, 消除了随机测试作为过滤阶段和 SMT 解答器的需要。 因此, 它可以进行易懂的构成推理, 并处理用户定义的更高排序的功能。 我们的实施显示, 在避免冗余的同时, 我们发现比以前的艺术更多的利玛。
相关内容
微信扫码咨询专知VIP会员