Output details
11 - Computer Science and Informatics
University of Kent
Article title
A pearl on SAT and SMT solving in Prolog
Type
D - Journal article
Title of journal
Theoretical Computer Science
Article number
-
Volume number
435
Issue number
-
First page of article
43
ISSN of journal
03043975
Year of publication
2012
URL
-
Number of additional authors
1
Additional information
<07> This paper is an extended version of a best paper from FLOPS’10. It shows how a constraint library, when combined with control primitives and backtracking, can be used to construct a SMT solver in Prolog. A follow-on paper in PPDP’13 explains how the SMT solver can be tuned to solve problems of over 250K clauses and 150K propositional variables that arise when recovering types from C executables. Recursive types are recovered by generating type constraints for each low-level instruction; the SMT solver is then deployed to find a type assignment that is compatible with all these constraints.
Interdisciplinary
-
Cross-referral requested
-
Research group
P - Programming Languages and Systems Group
Citation count
2
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
