Automated Deduction for Verification

被引：20
作者：
Shankar, Natarajan [1 ]
机构：
[1] SRI Int, Comp Sci Lab, Menlo Pk, CA 94025 USA
来源：
ACM COMPUTING SURVEYS | 2009年 / 41卷 / 04期
基金：
美国国家科学基金会;
关键词：
Theory; Verification; SYMBOLIC MODEL CHECKING; MODULO THEORIES; PROOF; SAT; PROGRAM; LOGIC; TOOL; SYSTEMS; COMBINATIONS; ABSTRACTION;
D O I：
10.1145/1592434.1592437
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Automated deduction uses computation to perform symbolic logical reasoning. It has been a core technology for program verification from the very beginning. Satisfiability solvers for propositional and first-order logic significantly automate the task of deductive program verification. We introduce some of the basic deduction techniques used in software and hardware verification and outline the theoretical and engineering issues in building deductive verification tools. Beyond verification, deduction techniques can also be used to support a variety of applications including planning, program optimization, and program synthesis.
引用
收藏
页数：56
相关论文
共 323 条
[1]   General decidability theorems for infinite-state systems [J].
Abdulla, PA ;
Cerans, K ;
Jonsson, B ;
Tsay, YK .
11TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 1996, :313-321
[2]  
ABRAMSKY S, 1992, HDB LOGIC COMPUTER S, V1
[3]  
Abrial J., 1980, SPECIFICATION LANGUA
[4]  
Abrial Jean-Raymond, 1996, The B-Book - Assigning Programs to Meanings
[5]  
Adams T., 1990, POLICE FIELD OPERATI
[6]  
Amla N, 2005, LECT NOTES COMPUT SC, V3725, P254
[7]  
ANDREWS PB, 1988, LECT NOTES COMPUT SC, V310, P760, DOI 10.1007/BFb0012885
[8]  
ANDREWS PB, 1986, INTRO LOGIC TYPE THE
[9]  
[Anonymous], U SERIES UNDERGRADUA
[10]  
[Anonymous], 1983, Automation of Reasoning
12345678910