Software Verification using Predicate Abstraction and Iterative Refinement Part 1 15 414 Bug Catching Automated Program Verification and Testing Sagar Chaki November 28 2011 2006 Carnegie Mellon University Outline Overview of Model Checking Creating Models from C Code Predicate Abstraction Eliminating spurious behaviors from the model Abstraction Refinement Concluding remarks research directions tools etc Software Verification Sagar Chaki March 16 2011 2006 Carnegie Mellon University 2 Model Checking Algorithm for answering queries about behaviors of state machines Given a state machine M and a query does M Standard formulation M is a Kripke structure is a temporal logic formula Computational Tree Logic CTL Linear Temporal Logic LTL Discovered independently by Clarke Emerson and Queille Sifakis in the early 1980 s Software Verification Sagar Chaki March 16 2011 2006 Carnegie Mellon University 3 Scalability of Model Checking Explicit statespace exploration early 1980s Tens of thousands of states Symbolic statespace exploration millions of states Binary Decision Diagrams BDD early 1990 s Bounded Model Checking late 1990 s Based on propositional satisfiability SAT technology Abstraction and compositional reasoning 10120 to effectively infinite statespaces particularly for software Software Verification Sagar Chaki March 16 2011 2006 Carnegie Mellon University 4 Models of C Code if x y x else if x no x 0 y 0 x 1 y 0 yes y x 1 y x x 1 y 0 x 0 y 0 y x 1 assert y assert y Program Syntax Control Flow Graph x 0 y 1 x 1 y 1 Model Semantics Infinite State Software Verification Sagar Chaki March 16 2011 2006 Carnegie Mellon University 5 Existential Abstraction Partition concrete statespace into abstract states Each abstract state S corresponds to a set of concrete states s We write s to mean the abstract state corresponding to s We define S s S s Fix the transitions existentially S S S S 9 s 2 S 9 s 2 S s s 9 s 2 S 9 s 2 S s s Strong sometimes not computable Weak computable Existential Abstraction is conservative ClarkeGrumbergLong94 If a ACTL property holds on the abstraction it also holds on the program LTL is a subset of ACTL However the converse is not true a property that fails on the abstraction may still hold on the program Existential abstraction can be viewed as a form of abstract interpretation Software Verification Sagar Chaki March 16 2011 2006 Carnegie Mellon University 6 Example of Existential Abstraction Abstract Initial State Concrete Initial State Concrete State 6 2 1 8 5 9 Concrete Transition 3 Abstractly Reachable but Concretely Unreachable Abstract State 4 10 7 Abstract Transition Abstractly and Concretely Unreachable Software Verification Sagar Chaki March 16 2011 2006 Carnegie Mellon University 7 Example of Existential Abstraction Concrete State Abstract State Concrete Transition Abstractly Reachable but Concretely Unreachable Abstractly and Concretely Unreachable p Abstract Transition G p Software Verification Sagar Chaki March 16 2011 2006 Carnegie Mellon University 8 Predicate Abstraction if x no yes y x 1 assert y y x Partition the statespace based on values of a finite set of predicates on program variables Software Verification Sagar Chaki March 16 2011 2006 Carnegie Mellon University 9 Predicate Abstraction G ERROR if x no yes y x 1 y x ERROR assert y P States where y 0 P P y 0 States where y 0 Software Verification Sagar Chaki March 16 2011 2006 Carnegie Mellon University 10 Predicate Abstraction if x no Call SAT Checker yes y x 1 y x ERROR assert y P States where y 0 P P y 0 States where y 0 Software Verification Sagar Chaki March 16 2011 2006 Carnegie Mellon University 11 Predicate Abstraction SAT Checker Query if x no y 0 x 0 y 1 x 0 yes y x 1 y x x x y y x 0 y 1 y 0 SAT Checker Answer SAT and here s a solution assert y x 0 y 1 x 0 y 1 P States where y 0 P y 0 Software Verification Sagar Chaki March 16 2011 2006 Carnegie Mellon University 12 Predicate Abstraction SAT Checker Query if x no y 0 x 1 y 1 x 0 yes y x 1 x x y x y y x 1 y 1 y 0 SAT Checker Answer SAT and here s a solution assert y x 1 y 1 x 1 y 1 P States where y 0 P y 0 Software Verification Sagar Chaki March 16 2011 2006 Carnegie Mellon University 13 Predicate Abstraction if x no SAT Checker Query yes y 0 x x y x 1 y x x 1 y 1 y x 1 y 0 SAT Checker Answer assert y x 1 y 2 SAT and here s a solution x 1 y 1 x 1 y 2 P States where y 0 P y 0 Software Verification Sagar Chaki March 16 2011 2006 Carnegie Mellon University 14 Predicate Abstraction if x no SAT Checker Query yes y 0 x x y x 1 y x x 1 y 1 y x y 0 SAT Checker Answer assert y x 1 y 1 SAT and here s a solution x 1 y 1 x 1 y 1 P States where y 0 P y 0 Software Verification Sagar Chaki March 16 2011 2006 Carnegie Mellon University 15 Predicate Abstraction No predicates about x if x no yes y x 1 y x ERROR assert y P States where y 0 P P y 0 States where y 0 Software Verification Sagar Chaki March 16 2011 2006 Carnegie Mellon University 16 Imprecision due to Predicate Abstraction Counterexamples generated by model checking the abstract model may be spurious i e not concretely realizable Need to refine the abstraction iteratively by changing the set of predicates Can infer new set of predicates by analyzing the spurious counterexample Lot of research in doing this effectively Counterexample Guided Abstraction Refinement CEGAR A K A Iterative Abstraction Refinement A K A Iterative Refinement Software Verification Sagar Chaki March 16 2011 2006 Carnegie Mellon University 17 Model Checking if x no yes y x 1 y x ERROR assert y P G ERROR P P y 0 Software Verification Sagar Chaki March 16 2011 2006 Carnegie Mellon University 18 Model Checking if x no yes y x 1 y x ERROR assert y P G ERROR P P y 0 Software Verification Sagar Chaki March 16 2011 2006 Carnegie Mellon University 19 Model Checking if x yes y x ERROR assert y P P P y 0 Software Verification Sagar Chaki March 16 2011 2006 Carnegie Mellon University 20 Counterexample Validation if x yes y x Simulate counterexample symbolically Call SAT Checker to determine if the post condition is satisfiable In our case Counterexample is spurious assert y New set of predicates x 0 y 0 Software Verification Sagar Chaki March 16 2011 2006 Carnegie Mellon University 21 Counterexample Validation SAT Checker Query x 0 if x yes y x y x y 0 SAT Checker Answer UNSAT and here s an UNSAT core x 0 y x y 0 assert y Used to derive new predicate x 0 Different heuristics used …