Title :
Algorithms for software model checking: Predicate abstraction vs. Impact
Author :
Beyer, Dagmar ; Wendler, Philipp
Author_Institution :
Univ. of Passau, Passau, Germany
Abstract :
CEGAR, SMT solving, and Craig interpolation are successful approaches for software model checking. We compare two of the most important algorithms that are based on these techniques: lazy predicate abstraction (as in Blast) and lazy abstraction with interpolants (as in Impact). We unify the algorithms formally (by expressing both in the CPA framework) as well as in practice (by implementing them in the same tool). This allows us to flexibly experiment with new configurations and gain new insights, both about their most important differences and commonalities, as well as about their performance characteristics. We show that the essential contribution of the Impact algorithm is the reduction of the number of refinements, and compare this to another approach for reducing refinement effort: adjustable-block encoding (ABE).
Keywords :
data structures; formal verification; interpolation; refinement calculus; ABE; CEGAR; Craig interpolation; IMPACT algorithm; SMT solving; adjustable-block encoding; lazy abstraction with interpolants; lazy predicate abstraction; performance characteristics; predicate abstraction; refinement number; software model checking; Abstracts; Algorithm design and analysis; Concrete; Encoding; Model checking; Software; Software algorithms; Formal Verification; Interpolation; Large-Block Encoding; Lazy Abstraction; Predicate Abstraction; Refinement Techniques; Software Model Checking;
Conference_Titel :
Formal Methods in Computer-Aided Design (FMCAD), 2012
Conference_Location :
Cambridge
Print_ISBN :
978-1-4673-4832-4