zbMATH — the first resource for mathematics

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].

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