REFINITY to Model and Prove Program Transformation Rules
REFINITY to Model and Prove Program Transformation Rules
复制标题
REFINITY 用于建模和证明程序转换规则
DOI：
--
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Dominic Steinhöfel
中科院分区：
文献类型：
--
作者：
Dominic Steinhöfel
。REFINITY是一个工作台，用于对Java程序上的语句级转换规则进行建模，目的是正式验证它们的正确性。它基于抽象执行，一个具有高度证明自动化的抽象程序验证框架，并与关键程序证明器接口。我们描述了REFINITY的用户界面和功能，并说明了它在应用程序中证明代码重构规则的条件正确性的能力。
. REFINITY is a workbench for modeling statement-level transformation rules on Java programs with the aim to formally verify their correctness. It is based on Abstract Execution, a verification framework for abstract programs with a high degree of proof automation, and interfaces with the KeY program prover. We describe the user interface and functionality of REFINITY , and illustrate its capabilities along the application to proving conditional correctness of a code refactoring rule.
CakeML 的新的经过验证的编译器后端
DOI：
10.1145/2951913.2951924
发表时间：
2016
期刊：
--
影响因子：
--
作者：
Tan Y
通讯作者：
Tan Y