DOC PREVIEW
CMU CS 15414 - Software Verification using Predicate Abstraction and Iterative Refinement: Part 1

This preview shows page 1-2-17-18-19-35-36 out of 36 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 36 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 36 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 36 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 36 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 36 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 36 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 36 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 36 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

Software Verification using Predicate Abstraction and Iterative Refinement: Part 1© 2006 Carnegie Mellon University15-414 Bug Catching: Automated Program Verification and TestingSagar ChakiNovember 28, 2011OutlineOverview of Model CheckingCreating Models from C Code: Predicate AbstractionEliminating spurious behaviors from the model: Abstraction Refinement2Software VerificationSagar Chaki, March 16, 2011© 2006 Carnegie Mellon UniversityEliminating spurious behaviors from the model: Abstraction RefinementConcluding remarks : research directions, tools etc.Model CheckingAlgorithm 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 logicformula3Software VerificationSagar Chaki, March 16, 2011© 2006 Carnegie Mellon University•φis a temporal logicformula— Computational Tree Logic (CTL)— Linear Temporal Logic (LTL)Discovered independently by Clarke & Emerson and Queille & Sifakisin the early 1980’sScalability of Model CheckingExplicit statespace exploration: early 1980s• Tens of thousands of statesSymbolic statespace exploration: millions of states• Binary Decision Diagrams (BDD) : early 1990’s4Software VerificationSagar Chaki, March 16, 2011© 2006 Carnegie Mellon University• Bounded Model Checking: late 1990’s— Based on propositional satisfiability (SAT) technologyAbstraction and compositional reasoning• 10120to effectively infinite statespaces (particularly for software)Models of C Codeif (x) {y = x;} else {y = x + 1;y = x + 1if (x)y = xno yesx=1 y=0x=0 y=0x=0 y=0x=1 y=0…5Software VerificationSagar Chaki, March 16, 2011© 2006 Carnegie Mellon Universityy = x + 1;}assert (y);Program: Syntax Control Flow Graphassert (y)Model: Semanticsx=1 y=1x=0 y=1…Infinite StateExistential AbstractionPartition 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) . ∃ s’ ∈ γ (S’) . s → s’γγStrong & sometimes not computableWeak: computable6Software VerificationSagar Chaki, March 16, 2011© 2006 Carnegie Mellon University• S → S’ ⇐ ∃ s ∈γ(S) . ∃ s’ ∈γ(S’) . s → s’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 interpretationWeak: computableExample of Existential Abstraction216598Concrete StateAbstract StateConcrete Initial StateAbstract Initial State7Software VerificationSagar Chaki, March 16, 2011© 2006 Carnegie Mellon University34710Concrete TransitionAbstract TransitionAbstractly and Concretely UnreachableAbstractly Reachable but Concretely UnreachableExample of Existential AbstractionConcrete StateAbstract State8Software VerificationSagar Chaki, March 16, 2011© 2006 Carnegie Mellon UniversitypConcrete TransitionAbstract TransitionAbstractly and Concretely UnreachableAbstractly Reachable but Concretely UnreachableG(¬¬¬¬ p)Predicate Abstractiony = x + 1if (x)y = xno yesPartition the statespace based on values of a 9Software VerificationSagar Chaki, March 16, 2011© 2006 Carnegie Mellon Universityassert (y)based on values of a finite set of predicateson program variablesPredicate Abstractiony = x + 1if (x)y = xno yesφφφφ = GGGG(¬¬¬¬ ERROR)10Software VerificationSagar Chaki, March 16, 2011© 2006 Carnegie Mellon Universityassert (y)PPPP ≡≡≡≡ ( y == 0 )¬¬¬¬PPPPStates where y ≠≠≠≠ 0PPPPStates where y = 0ERRORPredicate Abstractiony = x + 1if (x)y = xno yesCall SAT Checker11Software VerificationSagar Chaki, March 16, 2011© 2006 Carnegie Mellon Universityassert (y)PPPP ≡≡≡≡ ( y == 0 )¬¬¬¬PPPPStates where y ≠≠≠≠ 0PPPPStates where y = 0ERRORPredicate Abstractiony = x + 1if (x)y = xno yesx=0 y=1x=0 y=1SAT Checker Query:y ≠≠≠≠ 0 ∧∧∧∧x = 0 ∧∧∧∧x’ = x ∧∧∧∧y’ = y ∧∧∧∧y’ ≠≠≠≠012Software VerificationSagar Chaki, March 16, 2011© 2006 Carnegie Mellon Universityassert (y)PPPP ≡≡≡≡ ( y == 0 )¬¬¬¬PPPPStates where y ≠≠≠≠ 0y’ ≠≠≠≠0SAT Checker Answer:SAT and here’s a solutionx=0, y=1, x’=0, y’=1Predicate Abstractiony = x + 1if (x)y = xno yesx=1 y=1x=1 y=1SAT Checker Query:y ≠≠≠≠ 0 ∧∧∧∧x ≠≠≠≠ 0 ∧∧∧∧x’ = x ∧∧∧∧y’ = y ∧∧∧∧y’ ≠≠≠≠013Software VerificationSagar Chaki, March 16, 2011© 2006 Carnegie Mellon Universityassert (y)P P P P ≡≡≡≡ ( y == 0 )¬¬¬¬PPPPStates where y ≠≠≠≠ 0y’ ≠≠≠≠0SAT Checker Answer:SAT and here’s a solutionx=1, y=1, x’=1, y’=1Predicate Abstractiony = x + 1if (x)y = xno yesx=1 y=1SAT Checker Query:y ≠≠≠≠ 0 ∧∧∧∧x’ = x ∧∧∧∧y’ = x+1 ∧∧∧∧14Software VerificationSagar Chaki, March 16, 2011© 2006 Carnegie Mellon Universityassert (y)PPPP ≡≡≡≡ ( y == 0 )¬¬¬¬PPPPStates where y ≠≠≠≠ 0x=1 y=2y’ ≠≠≠≠ 0SAT Checker Answer:SAT and here’s a solutionx=1, y=1, x’=1, y’=2Predicate Abstractiony = x + 1if (x)y = xno yesx=1 y=1SAT Checker Query:y ≠≠≠≠ 0 ∧∧∧∧x’ = x ∧∧∧∧y’ = x ∧∧∧∧15Software VerificationSagar Chaki, March 16, 2011© 2006 Carnegie Mellon Universityassert (y)PPPP ≡≡≡≡ ( y == 0 )¬¬¬¬PPPPStates where y ≠≠≠≠ 0x=1 y=1y’ ≠≠≠≠ 0SAT Checker Answer:SAT and here’s a solutionx=1, y=1, x’=1, y’=1Predicate Abstractiony = x + 1if (x)y = xno yesNo predicates about x16Software VerificationSagar Chaki, March 16, 2011© 2006 Carnegie Mellon Universityassert (y)PPPP ≡≡≡≡ ( y == 0 )¬¬¬¬PPPPStates where y ≠≠≠≠ 0PPPPStates where y = 0ERRORImprecision due to Predicate AbstractionCounterexamples generated by model checking the abstract model may be spurious, i.e., not concretely realizableNeed to refine the abstraction iteratively by changing the set of predicates17Software VerificationSagar Chaki, March 16, 2011© 2006 Carnegie Mellon UniversityCan infer new set of predicates by analyzing the spurious counterexample• Lot of


View Full Document

CMU CS 15414 - Software Verification using Predicate Abstraction and Iterative Refinement: Part 1

Download Software Verification using Predicate Abstraction and Iterative Refinement: Part 1
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Software Verification using Predicate Abstraction and Iterative Refinement: Part 1 and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Software Verification using Predicate Abstraction and Iterative Refinement: Part 1 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?