Verification and Synthesis using SMT Solvers
VS
3
:
V
erification and
S
ynthesis using
S
MT
S
olvers
SMT Solvers for Program Verification
Saurabh Srivastava
*
Sumit Gulwani **
Jeffrey S. Foster
*
*
University of Maryland, College Park
** Microsoft Research, Redmond
What VS
3
will let you do!
A. Discover invariants with arbitrary
quantification and boolean structure
–
∀
: E.g. Sortedness
–
∀∃
: E.g. Permutation
Selection Sort:
for i = 0…n
{for j = i…n
{find min index
}
if (min ≠ i)
swap A[min], A[i]
}
Selection Sort:
What VS
3
will let you do!
A. Discover invariants with arbitrary
quantification and boolean structure
–
∀
: E.g. Sortedness
–
∀∃
: E.g. Permutation
Selection Sort:
Output
array
i<n
j<n
Find min
index
if (min != i)
swap A[i], A[min]
i:=0
j:=i
Verification: Proving Programs Correct
Selection Sort:
Output
array
i<n
j<n
Find min
index
if (min != i)
swap A[i], A[min]
i:=0
j:=i
Verification: Proving Programs Correct
Selection Sort:
Output
array
i<n
j<n
Find min
index
if (min != i)
swap A[i], A[min]
i:=0
j:=i
Verification: Proving Programs Correct
Selection Sort:
Output
array
i<n
j<n
Find min
index
if (min != i)
swap A[i], A[min]
i:=0
j:=i
Verification: Proving Programs Correct
Bubble Sort:
Output
array
i>0
j<i
if (a[j] > a[j+1])
swap A[j], A[j+1]
i:=n-1
j:=0
Verification: Proving Programs Correct
User Input:Templates and Predicates
•
Templates
–
Intuitive and simple
•
Depending on the property being proved; form straight-forward
•
Limited to the quantification and disjunction
–
E.g., {i<j, i>j, i≤j, i≥j… }–
Enumerate predicates of the form
•
Predicate Abstraction
Tool architecture
C Program
Templates for
invariants
Predicate Sets
CFG
Cut-Set
Preconditions
Postconditions
Invariants
Fixed-point Computation
•
Constraint-based (VMCAI’09)
–
Separately encode each VC as SAT constraint
•
Local constraints
SAT clauses
–
Use SAT solver to do fixed-point computation
–
Compare against trivial approach: 1.6e14 minutes
•
Iterative (PLDI’09)
–
Facts do not form a lattice, but power-set does
–
We ensure that if there exists an invariant we find it
–
Intelligent lattice search: SMT solver for tx-functions
Weakest Preconditions
Weakest conditions
on input?
Example analyses
•
Tool can verify:
–
Sorting algorithms:
•
Selection, Insertion, Bubble, Quick, Merge Sort
–
Properties
•
Output is Sorted
•
Output contains
all
and
only
elements from the input
•
Tool can infer preconditions:
–
Worst case input (precondition) for sorting:
•
Reverse sorted array, all but Selection Sort
•
Selection Sort: sorted array except last elem is smallest
–
Inputs for functional correctness:
•
Binary search requires sorted array
•
Merge in merge sort expect sorted inputs
•
Missing initializers
Selection Sort:
Output
array
i<n
j<n
Find min
index
if (min != i)
swap A[i], A[min]
i:=0
j:=i
Demo: Selection Sort
Demo: Program
Demo: Output
Conclusions
•
VS
3
: Verification tool over predicate abstraction
•
Verification
–
Can infer quantified invariants
•
Maximally-weak preconditions
•
Builds on SMT Solvers, so exploits their power
•
Project Webpage
http://www.cs.umd.edu/~saurabhs/pacs
Recent extension:
Synthesis
•
Verification tool for quantified invariants
–
Reasoning about full functional specifications possible
•
What if we had missing program fragments?
–
Still possible to verify if we allow the tool to plug-in
equality predicates over program variables
–
Equality predicates translated to statements
•
We can synthesize
–
Strassen’s Matrix Multiplication!
–
Sorting algorithms!
This paper explores the use of SMT solvers for program verification and synthesis, focusing on discovering invariants with arbitrary quantification and boolean structure. It delves into proving programs correct by inferring program states and discusses tasks like sortedness and permutation. The authors present methodologies for verifying and synthesizing programs by leveraging SMT solvers to find invariants and ensure program correctness.
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.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
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.
E N D
Presentation Transcript
VS3: Verification and Synthesis using SMT Solvers SMT Solvers for Program Verification Saurabh Srivastava * Sumit Gulwani ** Jeffrey S. Foster * * University of Maryland, College Park ** Microsoft Research, Redmond
What VS3will let you do! A. Discover invariants with arbitrary quantification and boolean structure : E.g. Sortedness Selection Sort: for i = 0 n { for j = i n { find min index } if (min i) swap A[min], A[i] } .. k1,k2 k1 k2 : E.g. Permutation Aold .... j k Anew k j
What VS3 will let you do! A. Discover invariants with arbitrary quantification and boolean structure : E.g. Sortedness Selection Sort: i:=0 i<n .. k1,k2 k1 k2 j:=i j<n : E.g. Permutation Output array Find min index Aold .... j k if (min != i) swap A[i], A[min] Anew k j
Verification: Proving Programs Correct Input state true Selection Sort: i:=0 Iouter i<n j:=i Output state Iinner j<n Sortedness Permutation Output array Find min index The difficult task is program state (invariant) inference: Iinner, Iouter, Input state, Output state if (min != i) swap A[i], A[min]
Verification: Proving Programs Correct Input state true Selection Sort: k1,k2 : 0 k1<k2<n k1<i => A[k1] A[k2] i:=0 i < j i min < n i<n j:=i k1,k2 : 0 k1<k2<n k1<i => A[k1] A[k2] Output state k2 : 0 k2 i k2<j => A[min] A[k2] j<n Sortedness Permutation Output array Find min index The difficult task is program state (invariant) inference: Iinner, Iouter, Input state, Output state k1,k2 : 0 k1<k2<n => A[k1] A[k2] if (min != i) swap A[i], A[min]
Verification: Proving Programs Correct Input state true Selection Sort: k1,k2 : (----------------) => A[k1] A[k2] k1,k2 : 0 k1<k2<n k1<i => A[k1] A[k2] k1,k2 : 0 k1<k2<n k1<i => A[k1] A[k2] i:=0 i < j (------------------- ) i min < n i<n j:=i k1,k2 : 0 k1<k2<n k1<i => A[k1] A[k2] k1,k2 : (---------------) => A[k1] A[k2] Output state k2 : 0 k2 i k2<j => A[min] A[k2] k2 : (-----------) => A[min] A[k2] j<n Sortedness Permutation Output array Find min index The difficult task is program state (invariant) inference: Iinner, Iouter, Input state, Output state k1,k2 : 0 k1<k2<n => A[k1] A[k2] if (min != i) swap A[i], A[min]
Verification: Proving Programs Correct Input state true Selection Sort: (------------------- ) k1,k2 : (----------------) => A[k1] A[k2] k2 : (-----------) => A[min] A[k2] i:=0 (------------------- ) i<n j:=i k1,k2 : (---------------) => A[k1] A[k2] Output state k2 : (-----------) => A[min] A[k2] j<n Sortedness Permutation Output array Find min index The difficult task is program state (invariant) inference: Iinner, Iouter, Input state, Output state k1,k2 : 0 k1<k2<n => A[k1] A[k2] if (min != i) swap A[i], A[min]
Verification: Proving Programs Correct Bubble Sort: (------------------- ) k1,k2 : (----------------) => A[k1] A[k2] k1,k2 : (----------) => A[k1] A[k2] i:=n-1 (------------------- ) i>0 j:=0 k1,k2 : (---------------) => A[k1] A[k2] k1,k2 : (----------) => A[k1] A[k2] j<i Output array if (a[j] > a[j+1]) swap A[j], A[j+1] k1,k2 : 0 k1<k2<n => A[k1] A[k2]
User Input:Templates and Predicates Templates Unknown holes Intuitive and simple Depending on the property being proved; form straight-forward Limited to the quantification and disjunction Predicate Abstraction Enumerate predicates of the form Program variables, array elements Relational operator <, , >, E.g., {i<j, i>j, i j, i j }
Tool architecture Microsoft s Phoenix Compiler Cut-Set VS3 Verification Conditions C Program CFG Templates for invariants Iterative Fixed-point GFP/LFP Constraint- based Fixed-Point Predicate Sets SMT Solver Candidate Solutions Boolean Constraint SAT Solver Preconditions Postconditions Invariants
Fixed-point Computation Constraint-based (VMCAI 09) Separately encode each VC as SAT constraint Local constraints SAT clauses Use SAT solver to do fixed-point computation Compare against trivial approach: 1.6e14 minutes Iterative (PLDI 09) Facts do not form a lattice, but power-set does We ensure that if there exists an invariant we find it Intelligent lattice search: SMT solver for tx-functions
Weakest Preconditions Weakest conditions on input? k2 k1 < i:=0 i<n j:=i Worst case behavior: swap every time it can j<n Output array Find min index if (min != i) swap A[i], A[min]
Example analyses Tool can verify: Sorting algorithms: Selection, Insertion, Bubble, Quick, Merge Sort Properties Output is Sorted Output contains all and only elements from the input Tool can infer preconditions: Worst case input (precondition) for sorting: Reverse sorted array, all but Selection Sort Selection Sort: sorted array except last elem is smallest Inputs for functional correctness: Binary search requires sorted array Merge in merge sort expect sorted inputs Missing initializers
Demo: Selection Sort Input state true Selection Sort: k1,k2 : 0 k1<k2<n k1<i => A[k1] A[k2] i:=0 i < j i min < n i<n j:=i k1,k2 : 0 k1<k2<n k1<i => A[k1] A[k2] Output state k2 : 0 k2 i k2<j => A[min] A[k2] j<n Sortedness Permutation Output array Find min index The difficult task is program state (invariant) inference: Iinner, Iouter, Input state, Output state k1,k2 : 0 k1<k2<n => A[k1] A[k2] if (min != i) swap A[i], A[min]
Conclusions VS3: Verification tool over predicate abstraction Verification Can infer quantified invariants Maximally-weak preconditions Builds on SMT Solvers, so exploits their power Project Webpage http://www.cs.umd.edu/~saurabhs/pacs Future work
Recent extension: Synthesis Verification tool for quantified invariants Reasoning about full functional specifications possible What if we had missing program fragments? Still possible to verify if we allow the tool to plug-in equality predicates over program variables Equality predicates translated to statements We can synthesize Strassen s Matrix Multiplication! Sorting algorithms!
