SPIN
2012
Springer
12 years 3 months ago
2012
Springer
Abstract. Craig interpolation is an active research topic and has become a powerful technique in verification. We present SMTInterpol, an interpolating SMT solver for the quanti...
CAV
2012
Springer
12 years 3 months ago
2012
Springer
Abstract. A minimum satisfying assignment of a formula is a minimumcost partial assignment of values to the variables in the formula that guarantees the formula is true. Minimum sa...
FROCOS
2011
Springer
13 years 12 days ago
2011
Springer
A dominant approach to Satisfiability Modulo Theories (SMT) relies on the integration of a Conflict-Driven-Clause-Learning (CDCL) SAT solver and of a decision procedure able to h...
PLDI
2011
ACM
13 years 3 months ago
2011
ACM
Program analysis and verification tools crucially depend on the ability to symbolically describe and reason about sets of program behaviors. Separation logic provides a promising...
ENTCS
2006
14 years 22 days ago
2006
To broaden the scope of decision procedures for linear arithmetic, they have to be integrated into theorem provers. Successful approaches e.g. in NQTHM or ACL2 suggest a close int...
CAV
2008
Springer
14 years 2 months ago
2008
Springer
Abstract. The use of Craig interpolants has enabled the development of powerful hardware and software model checking techniques. Efficient algorithms are known for computing interp...