Name
Abstract | ||
|---|---|---|
Recently, o-the-shelf Boolean SAT solvers have been used to construct ground decision procedures for various theories, including Quantier-F ree Presburger (QFP) arithmetic. One such approach (often called the eager approach) is based on a satisabilit y-preserving translation to a Boolean formula. Eager approaches are usually based on encoding integers as bit-vectors and suer from the loss of structure and sometime very large size for the bit-vectors. In this paper, we present a decision procedure for QFP that is based on alternately under and over-approximating a formula, where Boolean interpolants are used to compute the overapproximation. The novelty of the approach lies in using information from each phase (either underapproximation or overapproximation) to improve the other phase. Our preliminary experiments indicate that the algorithm consistently outperforms approaches based on eager and very lazy methods, on a set of verication benchmarks. In our experi- ence, the use of interpolants results in better abstractions being generated compared to an earlier method based on proofs directly. |
Year | Venue | Keywords |
|---|---|---|
2007 | JSAT | satisability modulo theories,interpolants,linear arithmetic,decision procedures,sat-solver,presburger arithmetic,sat solver,satisfiability modulo theories |
Field | DocType | Volume |
Integer,Discrete mathematics,Interpolation,Boolean satisfiability problem,Theoretical computer science,Presburger arithmetic,Mathematical proof,True quantified Boolean formula,Mathematics,Encoding (memory),Satisfiability modulo theories | Journal | 1 |
Issue | Citations | PageRank |
3-4 | 3 | 0.56 |
References | Authors | |
18 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Shuvendu K. Lahiri | 1 | 1424 | 68.18 |
| Krishna K. Mehra | 2 | 6 | 1.05 |