Lazy Abstraction with Interpolants

By Kenneth L. McMillan. International Conference on Computer Aided Verification, 2006

494 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Learning Shape Analysis (2017, methodology): “Similary, SplInter extends the Impact [30] safety prover with heap reasoning based on an interpolation technique for separation logic.”
Software model checking (2009, unknown): “This approach, which is implemented in the F-Soft [Jain et al. 2006] and Impact [McMillan 2006] model checkers, can make veriﬁcation much faster if if the ﬁrst phase can cheaply ﬁnd invariants that are crucial for the second phase, but which are expensive to compute using a more general abstraction…”