Program Verification Using Templates Over Predicate Abstraction
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. Sortedness
: E.g. Permutation
B. Infer weakest preconditions
Weakest
conditions
on input:
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
–
Task of inferring conjunctive facts for the holes remains
•
Predicate Abstraction
–
Allows us to efficiently compute solutions for the holes
–
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)
•
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)
•
Optimal Solutions
–
Built over a clean theorem proving interface
•
Weakest Precondition Generation
•
Experimental evaluation
Analysis Setup
post
pre
Loop headers (with invariants) split program
into simple paths. Simple paths induce
program constraints (verification conditions)
true
∧
i=0 => I
1
I
1
∧
i<n
∧
j=i => I
2
Analysis Setup
post
pre
Loop headers (with invariants) split program
into simple paths. Simple paths induce
program constraints (verification conditions)
Iterative Fixed-point: Overview
post
pre
Iterative Fixed-point: Overview
post
pre
Improve candidate
–
Pick unsat VC
–
Use theorem prover to
compute optimal change
–
Results in new candidates
Backwards Iterative (GFP)
post
pre
Backward:
•
Always pick the source invariant
of unsat constraint to improve
•
Start with <
⊤
,
…,
⊤
>
Backwards Iterative (GFP)
post
pre
✓
✓
Backward:
•
Always pick the source invariant
of unsat constraint to improve
•
Start with <
⊤
,
…,
⊤
>
✓
✗
✓
Backwards Iterative (GFP)
post
pre
✓
✓
Backward:
•
Always pick the source invariant
of unsat constraint to improve
•
Start with <
⊤
,
…,
⊤
>
✓
✗
✗
Backwards Iterative (GFP)
post
pre
✓
✓
✓
Backward:
•
Always pick the source invariant
of unsat constraint to improve
•
Start with <
⊤
,
…,
⊤
>
✓
✗
Backwards Iterative (GFP)
post
pre
✓
✓
✓
✓
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
Constraint-based over Predicate
Abstraction
pred(
I
1
)
Remember:
VCs are FOL
formulae
over I
1
, I
2
Constraint-based over Predicate
Abstraction
pred(
I
1
)
Remember:
VCs are FOL
formulae
over I
1
, I
2
Remember:
VCs are FOL
formulae
over I
1
, I
2
Constraint-based over Predicate
Abstraction
Optimal
solutions
from SMT
solver to
impose
minimal
constraints
Outline
•
Three fixed-point inference algorithms
–
Iterative fixed-point
•
Greatest Fixed-Point (GFP)
•
Least Fixed-Point (LFP)
–
Constraint-based (CFP)
•
Optimal Solutions
–
Built over a clean theorem proving interface
•
Weakest Precondition Generation
•
Experimental evaluation
Optimal Solutions
•
Key: Polarity of unknowns in formula
Φ
–
Positive or negative:
•
Value of positive unknown stronger =>
Φ
stronger
•
Value of negative unknown stronger =>
Φ
weaker
•
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
u
1
∨
u
2
)
∧
u
3
(
∀
x :
∃
y :
Φ =
Optimal Solutions using OptNegSol
formula
Φ
contains unknowns:
u
1
…u
P
positive
u
1
…u
N
negative
P x Size of predicate set
Outline
•
Three fixed-point inference algorithms
–
Iterative fixed-point
•
Greatest Fixed-Point (GFP)
•
Least Fixed-Point (LFP)
–
Constraint-based (CFP)
•
Optimal Solutions
–
Built over a clean theorem proving interface
•
Weakest Precondition Generation
•
Experimental evaluation
Computing maximally weak preconditions
•
Iterative:
–
Backwards algorithm:
•
Computes maximally-weak invariants in each step
–
Precondition generation using GFP:
•
Output disjuncts of entry fixed-point in all candidates
•
Constraint-based:
–
Generate one solution for precondition
–
Assert constraint that ensures strictly weaker pre
–
Iterate till unsat—last precondition generated is
maximally weakest
Outline
•
Three fixed-point inference algorithms
–
Iterative fixed-point
•
Greatest Fixed-Point (GFP)
•
Least Fixed-Point (LFP)
–
Constraint-based (CFP)
•
Optimal Solutions
–
Built over a clean theorem proving interface
•
Weakest Precondition Generation
•
Experimental evaluation
Implementation
C Program
Templates
Predicate Set
CFG
Invariants
Preconditions
Verification
Conditions
Iterative
Fixed-point
GFP/LFP
Constraint-
based
Fixed-Point
Candidate
Solutions
Boolean
Constraint
Verifying Sorting Algorithms
•
Benchmarks
–
Considered difficult to verify
–
Require invariants with quantifiers
–
Sorting, ideal benchmark programs
•
5 major sorting algorithms
–
Insertion Sort, Bubble Sort (n
2
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]=A
old
[j]
&
0
≤
j<n --- no elements gained
•
∀
k
∃
j :
0
≤
k<n => A
old
[k]=A[j]
&
0
≤
j<n --- no elements lost
Runtimes: Sortedness
seconds
Tool can prove
sortedness for all
sorting algorithms!
Runtimes: Permutation
seconds
…Permutations too!
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
seconds
Tool infers worst
case inputs for all
sorting algorithms!
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
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
