Name
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. Unlike most state-of-the-art array solvers, it is not based on a lazy instantiation of the array axioms. This novelty might make it more convenient to apply this solver in some particular environments. Moreover, it is very competitive in practice, specially on problems that require heavy reasoning on array literals. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1109/FMCAD.2008.ECP.18 | FMCAD |
Keywords | Field | DocType |
array literal,boolean engine,write-based solver,sat modulo,t-solver interacts,array axiom,state-of-the-art array solvers,equality literal,lazy instantiation,axiom instantiation,sat modulo theories,new t-solver,formal verification,hardware,engines,boolean functions,software verification,matrices,indexes,computability,mathematical model,computer algorithms,model theory | Boolean function,Programming language,Computer science,Modulo,Computability,Theoretical computer science,DPLL algorithm,Lazy initialization,Solver,Formal verification,Software verification | Conference |
Citations | PageRank | References |
7 | 0.54 | 12 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Miquel Bofill | 1 | 148 | 19.04 |
| Robert Nieuwenhuis | 2 | 1405 | 93.78 |
| Albert Oliveras | 3 | 1145 | 57.03 |
| Enric Rodríguez-Carbonell | 4 | 446 | 26.13 |
| Albert Rubio | 5 | 228 | 19.44 |