A Write-Based Solver for SAT Modulo the Theory of Arrays
dc.contributor.author
dc.date.accessioned
2013-10-03T10:43:57Z
dc.date.available
2013-10-03T10:43:57Z
dc.date.issued
2008
dc.identifier.isbn
978-1-4244-2735-2
dc.identifier.uri
dc.description.abstract
The extensional theory of arrays is one of the most important ones for applications of SAT Modulo Theories (SMT) to hardware and software verification. Here we present a new T-solver for arrays in the context of the DPLL(T) approach to SMT. The main characteristics of our solver are: (i) no translation of writes into reads is needed, (ii) there is no axiom instantiation, and (iii) the T-solver interacts with the Boolean engine by asking to split on equality literals between indices. As far as we know, this is the first accurate description of an array solver integrated in a state-of-the-art SMT solver and, unlike most state-of-the-art solvers, it is not based on a lazy instantiation of the array axioms. Moreover, it is very competitive in practice, specially on problems that require heavy reasoning on array literals
dc.format.mimetype
application/pdf
dc.language.iso
eng
dc.publisher
IEEE (Institute of Electrical and Electronics Engineers)
dc.relation.isformatof
Versió postprint del document publicat a: http://dx.doi.org/10.1109/FMCAD.2008.ECP.18
dc.relation.ispartof
© Formal Methods in Computer-Aided Design, 2008. FMCAD '08, 2008, p.1-8
dc.relation.ispartofseries
Articles publicats (D-IMA)
dc.rights
Tots els drets reservats
dc.subject
dc.title
A Write-Based Solver for SAT Modulo the Theory of Arrays
dc.type
info:eu-repo/semantics/article
dc.rights.accessRights
info:eu-repo/semantics/openAccess
dc.embargo.terms
Cap
dc.type.version
info:eu-repo/semantics/acceptedVersion
dc.identifier.doi
dc.identifier.idgrec
009847