Conference item icon

Conference item

An abstract interpretation of DPLL(T)

Abstract:

DPLL(T) is a central algorithm for Satisfiability Modulo Theories (SMT) solvers. The algorithm combines results of reasoning about the Boolean structure of a formula with reasoning about conjunctions of theory facts to decide satisfiability. This architecture enables modern solvers to combine the performance benefits of propositional satisfiability solvers and conjunctive theory solvers. We characterise DPLL(T) as an abstract interpretation algorithm that computes a product of two abstraction...

Expand abstract
Publication status:
Published
Peer review status:
Peer reviewed

Actions


Access Document


Files:
Publisher copy:
10.1007/978-3-642-35873-9_27

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Role:
Author

Contributors

Role:
Editor
Role:
Editor
Role:
Editor
Publisher:
Springer Publisher's website
Journal:
Lecture Notes in Computer Science: VMCAI 2013: Verification, Model Checking, and Abstract Interpretation Journal website
Volume:
7737
Pages:
455-475
Host title:
Lecture Notes in Computer Science: VMCAI 2013: Verification, Model Checking, and Abstract Interpretation
Publication date:
2013-01-01
DOI:
ISSN:
1611-3349 and 0302-9743
Source identifiers:
392834
ISBN:
9783642358722
Keywords:
Pubs id:
pubs:392834
UUID:
uuid:c21f8243-8316-4ccc-b266-85a4a80b8846
Local pid:
pubs:392834
Deposit date:
2017-01-28

Terms of use


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP