DocumentCode
3077098
Title
Approximating Quantified SMT-Solving with SAT
Author
Fu, Xianjin ; Liu, Wanwei ; Li, Jing
Author_Institution
Nat. Lab. for Parallel & Distrib. Process., Nat. Univ. of Defense Technol., Changsha, China
fYear
2011
fDate
27-29 June 2011
Firstpage
114
Lastpage
119
Abstract
Satisfiability Modulo Theories (SMT) is an extension of SAT towards FOL. SMT solvers have proven highly scalable and efficient for problems based on some ground theorems. However, SMT problems involving quantifiers and combination of theorems is a long-standing challenge, which has been a major bottleneck of practical application of SMT solvers in some fields. We reveal a decidable fragment of FOL involving quantifiers, which could not be solved by SMT solvers such as Z3, CVC3, etc., and show how to convert them into model checking problems.
Keywords
computability; formal verification; FOL; SAT; quantified SMT solvers; satisfiability modulo theories; Benchmark testing; Cognition; Computational modeling; Connectors; Encoding; Labeling; Semantics; Model Checking; SAT; Satisfiability Modulo Theories;
fLanguage
English
Publisher
ieee
Conference_Titel
Secure Software Integration & Reliability Improvement Companion (SSIRI-C), 2011 5th International Conference on
Conference_Location
Jeju Island
Print_ISBN
978-1-4577-0781-0
Electronic_ISBN
978-0-7695-4454-0
Type
conf
DOI
10.1109/SSIRI-C.2011.40
Filename
6004512
Link To Document