×

Lazy abstraction with interpolants. (English) Zbl 1188.68196

Ball, Thomas (ed.) et al., Computer aided verification. 18th international conference, CAV 2006, Seattle, WA, USA, August 17–20, 2006. Proceedings. Berlin: Springer (ISBN 3-540-37406-X/pbk). Lecture Notes in Computer Science 4144, 123-136 (2006).
Summary: We describe a model checker for infinite-state sequential programs, based on Craig interpolation and the lazy abstraction paradigm. On device driver benchmarks, we observe a speedup of up to two orders of magnitude relative to a similar tool using predicate abstraction.
For the entire collection see [Zbl 1114.68002].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI