Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
SPIN
2012
Springer
9 years 2 months ago
SMTInterpol: An Interpolating SMT Solver
Abstract. Craig interpolation is an active research topic and has become a powerful technique in veri´Čücation. We present SMTInterpol, an interpolating SMT solver for the quanti´Č...
Jürgen Christ, Jochen Hoenicke, Alexander Nut...
CAV
2012
Springer
227views Hardware» more  CAV 2012»
9 years 2 months ago
Minimum Satisfying Assignments for SMT
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...
Isil Dillig, Thomas Dillig, Kenneth L. McMillan, A...
FROCOS
2011
Springer
9 years 11 months ago
Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT
A dominant approach to Satis´Čüability Modulo Theories (SMT) relies on the integration of a Con´Čéict-Driven-Clause-Learning (CDCL) SAT solver and of a decision procedure able to h...
Alberto Griggio, Quoc-Sang Phan, Roberto Sebastian...
PLDI
2011
ACM
10 years 2 months ago
Separation logic + superposition calculus = heap theorem prover
Program analysis and veri´Čücation tools crucially depend on the ability to symbolically describe and reason about sets of program behaviors. Separation logic provides a promising...
Juan Antonio Navarro Pérez, Andrey Rybalche...
ENTCS
2006
125views more  ENTCS 2006»
10 years 11 months ago
An Even Closer Integration of Linear Arithmetic into Inductive Theorem Proving
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...
Tobias Schmidt-Samoa
CAV
2008
Springer
170views Hardware» more  CAV 2008»
11 years 1 months ago
Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
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...
Himanshu Jain, Edmund M. Clarke, Orna Grumberg
books