Sciweavers

ICCAD
2010
IEEE
140views Hardware» more  ICCAD 2010»
13 years 9 months ago
Reduction of interpolants for logic synthesis
Craig Interpolation is a state-of-the-art technique for logic synthesis and verification, based on Boolean Satisfiability (SAT). Leveraging the efficacy of SAT algorithms, Craig In...
John D. Backes, Marc D. Riedel
CADE
2010
Springer
14 years 19 days ago
An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
Craig interpolation has become a versatile tool in formal verification, for instance to generate intermediate assertions for safety analysis of programs. Interpolants are typically...
Angelo Brillout, Daniel Kroening, Philipp Rüm...
CSL
2009
Springer
14 years 6 months ago
Craig Interpolation for Linear Temporal Languages
We study Craig interpolation for fragments and extensions of propositional linear temporal logic (PLTL). We consider various fragments of PLTL obtained by restricting the set of te...
Amélie Gheerbrant, Balder ten Cate
POPL
2008
ACM
14 years 12 months ago
Relevance heuristics for program analysis
Relevance heuristics allow us to tailor a program analysis to a particular property to be verified. This in turn makes it possible to improve the precision of the analysis where n...
Kenneth L. McMillan