Checking equivalence in a non-strict language
Checking equivalence in a non-strict language
复制标题
检查非严格语言的等价性
DOI：
10.1145/3563340
复制
发表时间：
2022
影响因子：
--
通讯作者：
Hallahan, William T.
中科院分区：
文献类型：
--
作者：
Kolesar, John C.;Piskac, Ruzica;Hallahan, William T.
程序等价性检查是确认两个程序在相应的输入上具有相同的行为的任务。我们开发了一种基于符号执行和协归纳的演算来检验非严格函数语言中程序的等价性。此外，我们证明了我们的微积分可以用来推导对不等价程序的反例，包括由非终止产生的反例。我们描述了一种完全自动化的方法来寻找等价证明和反例。我们的实现Nebula证明了用Haskell编写的程序的等价性。通过将Nebula应用于现有的基准属性，我们证明了Nebula在证明等价性和自动生成反例方面的实际有效性。
Program equivalence checking is the task of confirming that two programs have the same behavior on corresponding inputs. We develop a calculus based on symbolic execution and coinduction to check the equivalence of programs in a non-strict functional language. Additionally, we show that our calculus can be used to derive counterexamples for pairs of inequivalent programs, including counterexamples that arise from non-termination. We describe a fully automated approach for finding both equivalence proofs and counterexamples. Our implementation, Nebula, proves equivalences of programs written in Haskell. We demonstrate Nebula's practical effectiveness at both proving equivalence and producing counterexamples automatically by applying Nebula to existing benchmark properties.
登录
查看更多内容
通用循环定理证明者
影响因子：
0.6
作者：
J. Brotherston;Nikos Gorogiannis;R. Petersen
通讯作者：
R. Petersen
DOI：
10.1007/978-3-540-45085-6_22
发表时间：
2003-07
期刊：
--
影响因子：
--
作者：
L. Dixon;Jacques D. Fleuriot
通讯作者：
L. Dixon;Jacques D. Fleuriot
CIRC : 圆形感应证明器
DOI：
--
发表时间：
2007
期刊：
Conference on Algebra and Coalgebra in Computer Science
影响因子：
--
作者：
D. Lucanu;Grigore Roşu
通讯作者：
Grigore Roşu
影响因子：
0.6
作者：
Grigore Roşu;D. Lucanu
通讯作者：
D. Lucanu
DOI：
10.1145/3314221.3314643
发表时间：
2018-08
期刊：
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Phuc C. Nguyen;Thomas Gilray;Sam Tobin-Hochstadt;David Van Horn
通讯作者：
Phuc C. Nguyen;Thomas Gilray;Sam Tobin-Hochstadt;David Van Horn