To access the full text documents, please follow this link: http://hdl.handle.net/10256/8405
| dc.contributor.author | Bofill Arasa, Miquel |
|---|---|
| dc.contributor.author | Nieuwenhuis, Robert |
| dc.contributor.author | Oliveras Llunell, Albert |
| dc.contributor.author | Rodríguez Carbonell, Enric |
| dc.contributor.author | Rubio, Albert |
| dc.date | 2008 |
| dc.identifier.citation | 978-1-4244-2736-9 (versió electrònica) |
| dc.identifier.citation | 978-1-4244-2735-2 (versió paper) |
| dc.identifier.citation | http://dx.doi.org/10.1109/FMCAD.2008.ECP.18 |
| dc.identifier.uri | http://hdl.handle.net/10256/8405 |
| 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 | application/pdf |
| dc.language.iso | eng |
| dc.publisher | IEEE (Institute of Electrical and Electronics Engineers) |
| dc.relation | Versió postprint del document publicat a: http://dx.doi.org/10.1109/FMCAD.2008.ECP.18 |
| dc.relation | © Formal Methods in Computer-Aided Design, 2008. FMCAD '08, 2008, p.1-8 |
| dc.relation | Articles publicats (D-IMA) |
| dc.rights | Tots els drets reservats |
| dc.subject | Algorismes computacionals |
| dc.subject | Computer algorithms |
| dc.subject | Models, Teoria dels |
| dc.subject | Model theory |
| dc.subject | Lògica matemàtica |
| dc.subject | Logic, Symbolic and mathematical |
| dc.subject | Matrius (Matemàtica) |
| dc.subject | Matrices |
| dc.title | A Write-Based Solver for SAT Modulo the Theory of Arrays |
| dc.type | info:eu-repo/semantics/article |
| dc.type | info:eu-repo/semantics/acceptedVersion |
Related documents
Other documents of the same author
Abío Roig, Ignasi; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric
Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto
Abío Roig, Ignasi; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric
Abío Roig, Ignasi; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Stuckey, Peter
Brockschmidt, Marc; Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto