Simplify: A theorem prover for program checking

被引：300
作者：
Detlefs, D
Nelson, G
Saxe, JB
机构：
[1] Sun Microsyst Labs, Burlington, MA 01803 USA
[2] Hewlett Packard Labs, Palo Alto, CA 94304 USA
来源：
JOURNAL OF THE ACM | 2005年 / 52卷 / 03期
关键词：
algorithms; verification; theorem proving; decision procedures; program checking;
D O I：
10.1145/1066100.1066102
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
This article provides a detailed description of the automatic theorem prover Simplify, which is the proof engine of the Extended Static Checkers ESC/Java and ESC/Modula-3. Simplify uses the Nelson-Oppen method to combine decision procedures for several important theories, and also employs a matcher to reason about quantifiers. Instead of conventional matching in a term DAG, Simplify matches up to equivalence in an E-graph, which detects many relevant pattern instances that would be missed by the conventional approach. The article describes two techniques, error context reporting and error localization, for helping the user to determine the reason that a false conjecture is false. The article includes detailed performance figures on conjectures derived from realistic program-checking problems.
引用
收藏
页码：365 / 473
页数：109
相关论文
共 34 条
[1]  
Badros G. J., 2001, ACM Transactions on Computer-Human Interaction, V8, P267, DOI 10.1145/504704.504705
[2]  
Conchon S, 2003, LECT NOTES COMPUT SC, V2619, P537
[3]  
de Moura L, 2004, LECT NOTES COMPUT SC, V3114, P162
[4]   VARIATIONS ON THE COMMON SUBEXPRESSION PROBLEM [J].
DOWNEY, PJ ;
SETHI, R ;
TARJAN, RE .
JOURNAL OF THE ACM, 1980, 27 (04) :758-771
[5]  
FLANAGAN C, 2002, P ACM SIGPLAN 2002 C, P234
[6]   AN IMPROVED EQUIVALENCE ALGORITHM [J].
GALLER, BA ;
FISHER, MJ .
COMMUNICATIONS OF THE ACM, 1964, 7 (05) :301-303
[7]  
Gulwani S, 2003, LECT NOTES ARTIF INT, V2741, P167
[8]  
Knuth D. E., 1978, Theoretical Computer Science, V6, P281, DOI 10.1016/0304-3975(78)90009-9
[9]  
Kozen Dexter, 1977, P 9 ANN ACM S THEORY, P164, DOI [10.1145/800105.803406, DOI 10.1145/800105.803406]
[10]  
McCarthy John, 1963, INFORM PROCESSING 62, P21
1234