Title :
Efficient implementation of property directed reachability
Author :
Een, Niklas ; Mishchenko, Alan ; Brayton, Robert
Author_Institution :
EECS Dept., Univ. of California, Berkeley, CA, USA
fDate :
Oct. 30 2011-Nov. 2 2011
Abstract :
Last spring, in March 2010, Aaron Bradley published the first truly new bit-level symbolic model checking algorithm since Ken McMillan´s interpolation based model checking procedure introduced in 2003. Our experience with the algorithm suggests that it is stronger than interpolation on industrial problems, and that it is an important algorithm to study further. In this paper, we present a simplified and faster implementation of Bradley´s procedure, and discuss our successful and unsuccessful attempts to improve it.
Keywords :
formal verification; interpolation; reachability analysis; Bradley procedure; bit-level symbolic model checking algorithm; interpolation based model checking procedure; property directed reachability; Algorithm design and analysis; Cognition; Engines; Interpolation; Reachability analysis; Syntactics; Vectors;
Conference_Titel :
Formal Methods in Computer-Aided Design (FMCAD), 2011
Conference_Location :
Austin, TX
Print_ISBN :
978-1-4673-0896-0
