Program Verification Using Templates Over Predicate Abstraction
This research explores a technique that allows for inferring invariants with arbitrary quantification and boolean structure, improving the state-of-the-art in program verification. It can infer weakest preconditions, helping with debugging and analysis by discovering worst-case inputs and missing precondition facts. The approach leverages templates and predicate abstraction to efficiently compute solutions for unknown holes and limited constants within programs, presenting three fixed-point inference algorithms for optimal solutions.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Program Verification using Templates over Predicate Abstraction Saurabh Srivastava University of Maryland, College Park Sumit Gulwani Microsoft Research, Redmond
What the technique will let you do! A. Infer invariants with arbitrary quantification and boolean structure : E.g. Permutation B. Infer weakest preconditions Weakest conditions on input: : E.g. Sortedness k2 k1 < Selection Sort: for i = 0..n { for j = i..n { } if (min != i) swap A[i] with A[min] } Worst case behavior: swap every time it can find min index Aold .... j .. k Anew k1,k2 k1 k2 k j
Improves the state-of-art Can infer very expressive invariants Quantification E.g. k j : (k<n) => (A[k]=B[j] j<n) Disjunction E.g. k : (k<0 k>n A[k]=0) Previous techniques are too specialized to particular types of quantification or to quantifier-free disjunction Can infer weakest preconditions Good for debugging: can discover worst case inputs Good for analysis: can infer missing precondition facts No satisfactory solutions known
Key facilitators Templates Unknown holes Task of inferring conjunctive facts for the holes remains Predicate Abstraction Allows us to efficiently compute solutions for the holes Limited constants Program variables, array elements Relational operator <, , >, Arithmetic operator +, - E.g., {i<j, i>j, i j, i j, i<j-1, i>j+1 }
Outline Three fixed-point inference algorithms Iterative fixed-point Greatest Fixed-Point (GFP) Least Fixed-Point (LFP) Constraint-based (CFP) (GFP) (CFP) (LFP) Optimal Solutions Built over a clean theorem proving interface Weakest Precondition Generation Experimental evaluation
Outline Three fixed-point inference algorithms Iterative fixed-point Greatest Fixed-Point (GFP) Least Fixed-Point (LFP) Constraint-based (CFP) (GFP) (CFP) (LFP)
Analysis Setup E.g. Selection Sort: pre true true i=0 => I1 i:=0 I1 vc(pre,I1) I1 i<n j=i => I2 I1 if (min != i) swap A[i], A[min] i<n vc(I1,post) Find min index j:=i I2 vc(I1,I2) I2 j<n Sorted array post vc(I2,I2) vc(I2,I1) I1 i n => sorted array Loop headers (with invariants) split program into simple paths. Simple paths induce program constraints (verification conditions)
Analysis Setup pre true i=0 => I1 vc(pre,I1) I1 i<n j=i => I2 I1 vc(I1,post) vc(I1,I2) Simple FOL formulae over I1, I2! We will exploit this. I2 post vc(I2,I2) vc(I2,I1) I1 i n => k1,k2 : 0 k1<k2<n => A[k1] A[k2] Loop headers (with invariants) split program into simple paths. Simple paths induce program constraints (verification conditions)
Iterative Fixed-point: Overview Candidate Solution Values for invariants pre <x,y> { vc(pre,I1),vc(I1,I2) } vc(pre,I1) I1 VCs that are not satisfied vc(I1,post) vc(I1,I2) I2 post vc(I2,I2) vc(I2,I1)
Iterative Fixed-point: Overview Improve candidate pre Candidate satisfies all VCs vc(pre,I1) I1 Set of candidates vc(I1,post) <x,y> { } vc(I1,I2) Improve candidate Pick unsat VC Use theorem prover to compute optimal change Results in new candidates I2 post vc(I2,I2) vc(I2,I1) Computable because: Templates make explicit Predicate abstraction restricts search to finite space
Backwards Iterative (GFP) Candidate Sols <I1,I2> Unsat constraints pre < , > { vc(I1,post) } post Backward: Always pick the source invariant of unsat constraint to improve Start with < , , >
Backwards Iterative (GFP) Optimally strengthen so vc(pre,I1) ok unless no soln Candidate Sols <I1,I2> Unsat constraints pre < , > { vc(I1,post) } a1 <a1, > { vc(I2,I1) } post Backward: Always pick the source invariant of unsat constraint to improve Start with < , , >
Backwards Iterative (GFP) Optimally strengthen so vc(pre,I1) ok unless no soln Candidate Sols <I1,I2> Unsat constraints pre < , > { vc(I1,post) } Multiple orthogonal optimal sols a1 <a1, > { vc(I2,I1) } <a1,b1> { vc(I2,I2) } <a1,b2> { vc(I2,I2),vc(I1,I2) } b2 post Backward: Always pick the source invariant of unsat constraint to improve Start with < , , >
Backwards Iterative (GFP) Optimally strengthen so vc(pre,I1) ok unless no soln Candidate Sols <I1,I2> Unsat constraints pre < , > { vc(I1,post) } Multiple orthogonal optimal sols a1 <a1, > { vc(I2,I1) } <a1,b1> { vc(I2,I2) } <a1,b2> { vc(I2,I2),vc(I1,I2) } <a1,b1> { vc(I2,I2) } <a1,b 2> { vc(I1,I2) } b 2 post Backward: Always pick the source invariant of unsat constraint to improve Start with < , , >
Backwards Iterative (GFP) Optimally strengthen so vc(pre,I1) ok unless no soln Candidate Sols <I1,I2> Unsat constraints pre < , > { vc(I1,post) } Multiple orthogonal optimal sols a 1 <a1, > { vc(I2,I1) } <a1,b1> { vc(I2,I2) } <a1,b2> { vc(I2,I2),vc(I1,I2) } <a1,b1> { vc(I2,I2) } <a1,b 2> { vc(I1,I2) } <a1,b1> { vc(I2,I2) } <a 1,b 2> none b 2 post <a 1,b 2> : GFP solution Backward: Always pick the source invariant of unsat constraint to improve Start with < , , >
Forward Iterative (LFP) Forward: Same as GFP except Pick the destination invariant of unsat constraint to improve Start with < , , >
Constraint-based over Predicate Abstraction pre vc(pre,I1) I1 vc(I1,post) vc(I1,I2) I2 post vc(I2,I2) vc(I2,I1)
Constraint-based over Predicate Abstraction pred(I1) vc(pre,I1) vc(I1,post ) vc(I1,I2) b11,b21 br1 b12,b22 br2 boolean indicators p1,p2 pr p1,p2 pr predicates vc(I2,I1) unknown 2 unknown 1 template vc(I2,I2) I1 Remember: VCs are FOL formulae over I1, I2
Constraint-based over Predicate Abstraction pred(A) : A to unknown predicate indicator variables pred(I1) vc(pre,I1) vc(I1,post ) vc(I1,I2) vc(I2,I1) vc(I2,I2) Remember: VCs are FOL formulae over I1, I2
Constraint-based over Predicate Abstraction SAT formulae over predicate indicators pred(A) : A to unknown predicate indicator variables Program constraint to boolean constraint Optimal solutions from SMT solver to impose minimal constraints boolc(pred(I1)) vc(pre,I1) boolc(pred(I1)) vc(I1,post ) vc(I1,I2) Invariant soln boolc(pred(I1), pred(I2)) boolc(pred(I2), pred(I1)) vc(I2,I1) boolc(pred(I2)) vc(I2,I2) Boolean constraint to satisfying soln (SAT Solver) Remember: VCs are FOL formulae over I1, I2 Fixed-Point Computation Local reasoning
Outline (GFP) (CFP) (LFP) Optimal Solutions Built over a clean theorem proving interface
Optimal Solutions Key: Polarity of unknowns in formula Positive or negative: Value of positive unknown stronger => stronger Value of negative unknown stronger => weaker negative positive u1 u2 ) u3 positive ( x : y : = Optimal Soln: Maximally strong positives, maximally weak negatives Assume theorem prover interface: OptNegSol Optimal solutions for formula with only negative unknowns Built using a lattice search by querying SMT Solver
Optimal Solutions using OptNegSol formula contains unknowns: u1 uP positive u1 uN negative Repeat until set stable OptNegSol P x Size of predicate set a1 aP,S1 SN a 1 a P,S 1 S N a1 aP a 1 a P [ [ ] Opt Opt Merge ] Opt a 1 a P,S 1 S N Optimal Solutions for formula a 1 a P [ ] P-tuple that assigns a single predicate to each positive unknown Merge positive tuples Si soln for the negative unknowns
Outline (GFP) (CFP) (LFP) Weakest Precondition Generation
Outline (GFP) (CFP) (LFP) Experimental evaluation
Implementation Microsoft s Phoenix Compiler Verification Conditions C Program CFG Templates Predicate Set Iterative Fixed-point GFP/LFP Constraint- based Fixed-Point Z3 SMT Solver Candidate Solutions Boolean Constraint Invariants Preconditions
Verifying Sorting Algorithms Benchmarks Considered difficult to verify Require invariants with quantifiers Sorting, ideal benchmark programs 5 major sorting algorithms Insertion Sort, Bubble Sort (n2 version and termination checking version), Selection Sort, Quick Sort and Merge Sort Properties: Sort elements k : 0 k<n => A[k] A[k+1] --- output array is non-decreasing Maintain permutation, when elements distinct k j : 0 k<n => A[k]=Aold[j] & 0 j<n --- no elements gained k j : 0 k<n => Aold[k]=A[j] & 0 j<n --- no elements lost
Runtimes: Sortedness 16 Tool can prove sortedness for all sorting algorithms! 14 12 10 seconds LFP 8 GFP CFP 6 4 2 0 Selection Sort Insertion Sort Bubble Sort (n2) Bubble Sort (flag) Quick Sort Merge Sort
Runtimes: Permutation 94.42 40 Permutations too! 35 30 25 seconds LFP 20 GFP CFP 15 10 5 0 Selection Sort Insertion Sort Bubble Sort (n2) Bubble Sort (flag) Quick Sort Merge Sort
Inferring Preconditions Given a property (worst case runtime or functional correctness) what is the input required for the property to hold Tool automatically infers non-trivial inputs/preconditions Worst case input (precondition) for sorting: Selection Sort: sorted array except last element is the smallest Insertion, Quick Sort, Bubble Sort (flag): Reverse sorted array Inputs (precondition) for functional correctness: Binary search requires sorted input array Merge in Merge sort requires sorted inputs Missing initializers required in various other programs
Runtimes (GFP): Inferring worst case inputs for sorting 45 Tool infers worst case inputs for all sorting algorithms! 40 35 30 seconds 25 Nothing to infer as all inputs yield the same behavior 20 15 10 5 0 Selection Sort Insertion Sort Bubble Sort (n2) Bubble Sort (flag) Quick Sort Merge Sort
Conclusions Powerful invariant inference over predicate abstraction Can infer quantifier invariants Three algorithms with different strengths Iterative: Least fixed-point and Greatest fixed-point Constraint-based Extend to maximally-weak precondition inference Worst case inputs Preconditions for functional correctness Techniques builds on SMT Solvers, so exploit their power Successfully verified/inferred preconditions All major sorting algorithms Other difficult benchmarks Project Webpage: http://www.cs.umd.edu/~saurabhs/pacs
