Lazy Abstraction with Interpolants

traction with Interpolants K. L. McMillan Cadence Berkeley Labs Abstract. We describe a model checker for infinite-state sequential proased on Craig interpolation and the lazy abstraction paradigm. On device driver benchmarks, we observe a speedup of up to two orders tude relative to a similar tool using predicate abstraction.

• Type: Conference
• Year: 2006
• Where: CAV
• Authors: Kenneth L. McMillan
• Keywords: CAV 2006, Device Driver Benchmarks, Hardware, Lazy Abstraction Paradigm, McMillan Cadence Berkeley