Effective Techniques for Automatic Program Synthesis and Verification

From Program Verification to Program Synthesis Saurabh Srivastava * Sumit Gulwani Jeffrey S. Foster * * University of Maryland, College Park Microsoft Research, Redmond

Program Synthesis Goal: Automatically generate program Important benefits of program synthesis Reduced programmer burden Potential to generate novel algorithms Objective: Automatic program synthesis, given Pre/post condition (functional specification) Some hints about the form of the program scaffold Ideally: program is automatically proved correct Synthesized programs can be complicated

Proof-theoretic synthesis Our approach: Synthesize program and proof simultaneously Benefits: Pruning invalid proofs prunes invalid programs E.g., A program that manipulates a ordered list Ordered list invariant has to hold, preventing any program that would violate it View synthesis as generalized verification Reuse existing verification tools and technology Tool synthesizes: linear arithmetic programs, sorting, dynamic programming programs

Discrete Line Drawing Input (X,Y) 0<Y X (12,7) (10,6) (11,6) (8,5) (9,5) (6,4) (7,4) Output values (5,3) |y-(Y/X)x| 1/2 (3,2) (4,2) (0,0) Using only linear operations: Bresenham s line drawing algorithm (0,0) (2,1) (1,1)

Scaffold(1): Functional Specification Precondition Fpre Formal specification of possible valid inputs E.g., 0<Y X Output Postcondition Fpost Formal specification that outputs need to meet E.g., |y-(Y/X)x| 1/2

Scaffold(2): Resource Constraints Hints about the form of the desired program Looping structure R loop Acyclic fragments (*), loops ( ), sequencing (;) Grammar: L ::= * | (L) | L;L * * E.g., R loop = *; (*) Acyclic fragment followed by a loop with an acyclic fragment inside Stack R stack Maximum number of local variables permitted E.g., R stack = 1 Only one extra local variable is available

Scaffold(3): Domains Domains for program elements Expressions Dexp Guards Dgrd E.g. linear or quadratic expression over program variables predicates with array lookups Domain for invariants Dprf Choice of solver E.g., linear arithmetic Invariant form: iaix+biy+ci 0 Linear arithmetic fixed-point computation tool, i.e., verifier

Outline Input: Scaffold Approach: Synthesis conditions Experiments

Modeling Basic Blocks as Transitions Task: Model statements in a manner that a solver can reason about State update and ordering problematic Basic Block as input->output transition inputs: v,x,Y outputs: v ,x v := v + 2Y; x++; transition : i(output vari = fn(input vars)) v = v + 2Y x = x + 1; Sbody :

Synthesis Task *; (*) expand 0<Y X Sinit while ( Gloop ) { |y-(Y/X)x| 1/2 []Gcond1 Sbody1 []Gcond2 Sbody2 Sinit while ( Gloop ) { output (x,y) []Gcond1 Sbody1 []Gcond2 Sbody2 } } Generate values for unknown Sinit/body1/body2,Gloop/cond Generate proof (invariants)

VC - Safety Constraints Verification condition (VC) 0<Y X Sinit I I Gloop |y-(Y/X)x| 1/2 I Gcond1 Sbody1 I I Gcond2 Sbody2 I entry: output: 0<Y X Sinit while ( Gloop ) { |y-(Y/X)x| 1/2 []Gcond1 Sbody1 []Gcond2 Sbody2 } induct: output I entry induct

Fixed point solutions, i.e., invariants Verification condition (VC) 0<Y X Sinit I I Gloop |y-(Y/X)x| 1/2 I Gcond1 Sbody1 I I Gcond2 Sbody2 I entry: output: verifier induct: Domain specific reducer SAT solver ik, i.e., invariant I Assume a form for I,e.g., i1x+i2y+i3 0 for I (given the domains) Gcond2 boolean clauses linear arithmetic i1x+i2y+i3 0 Sbody2 i1x +i2y +i3 0 Linear arithmetic tricks integer SAT instance ik: linear arithmetic [PLDI 08] predicate abstraction [PLDI 09]

Fixed point solutions, i.e., invariants Verification condition (VC) 0<Y X Sinit I I Gloop |y-(Y/X)x| 1/2 I Gcond1 Sbody1 I I Gcond2 Sbody2 I entry: output: verifier induct: Domain specific reducer SAT solver ik, i.e., invariant I Assume a form for I,e.g., i1x+i2y+i3 0 for I (given the domains) Gcond2 boolean clauses linear arithmetic i1x+i2y+i3 0 Sbody2 i1x +i2y +i3 0 Linear arithmetic tricks integer SAT instance ik: linear arithmetic [PLDI 08] predicate abstraction [PLDI 09]

Unknown statements and guards Synthesize statements and guards! Verification condition (VC) 0<Y X Sinit I I Gloop |y-(Y/X)x| 1/2 I Gcond1 Sbody1 I I Gcond2 Sbody2 I entry: output: verifier induct: Domain specific reducer SAT solver ik, i.e., invariant I Assume a form for I, Gcond2,Sbody2,e.g., i1x+i2y+i3 0 for I (given the domains) boolean clauses linear arithmetic i1x+i2y+i3 0 g1x+g2y+g3 0 x =s1x+s2y+s3 y = i1x +i2y +i3 0 gk and sk guards/ statements Linear arithmetic tricks integer SAT instance ik,gk,sk: linear arithmetic [PLDI 08] predicate abstraction [PLDI 09]

Statements unknown Trivial soln: Statements unknown: 0<Y X Sinit I I Gloop |y-(Y/X)x| 1/2 I Gcond1 Sbody1 I I Gcond2 Sbody2 I 0<Y X Sinit I I Gloop |y-(Y/X)x| 1/2 I Gcond1 Sbody1 I I Gcond2 Sbody2 I Ask solver But transitions, i.e., Sinit,Sbody1,Sbody2, cannot imply false Issue: Well-formedness not ensured Statements Conditional Guards Remember, statement unknowns: transition i(output vari = fn(input vars)) E.g., v = v + 2Y x = x + 1 Can never imply false Infer I and Sinit,Sbody1,Sbody2

Additional Constraints 0<Y X Sinit I I Gloop |y-(Y/X)x| 1/2 I Gcond1 Sbody1 I I Gcond2 Sbody2 I Termination Issue: Termination constraints Outputs reachable/termination constraints: Exists ranking function r r bounded from below r decreases in each iteration Safety Issue: Well-formedness not ensured Statements Well-formedness Conditional Guards Well-formedness constraints: Statement unknowns are not false Conditional guards form tautologies Infer I and Sinit,Sbody1,Sbody2,Gloop,Gcond

Additional Constraints Synthesis Conditions User input: Scaffold User input: Program 0<Y X Sinit I I Gloop |y-(Y/X)x| 1/2 I Gcond1 Sbody1 I I Gcond2 Sbody2 I Termination VCGen SCGen Safety Verification Conditions Synthesis Conditions Fixed-pt Solver Fixed-pt Solver Well-formedness Synthesized Program+ Proof Verified Program + Proof Synthesis Verification (Invariant inference) Infer I and (Invariant + Program inference) Sinit,Sbody1,Sbody2,Gloop,Gcond Solving synthesis conditions does yield valid programs

Example: Discrete Line Drawing Scaffol d Program: v := 2Y-X; y := 0; x := 0; while ( x X ) { print (x,y) if ( v<0 ) { v := v + 2Y; x++; } else { v := v + 2(Y-X); y++; x++; } } Invariant: 0<Y X v = 2(x+1)Y-(2y+1)X 2(Y-X) v 2Y Fpre Fpost : 0<Y X : 2|y-(Y/X)x| 1 R loop R stack : *; (*) Synthesis Conditions : one extra variable Constraint- based verifier Dexp Dgrd : linear arithmetic constraint-based linear arithmetic+ verifier Dprf : Ranking function: X-x Solution strategy (verifier) User Input Program and Proof

Outline Input: Scaffold Approach: Synthesis conditions Experiments

Experiments: Linear Arithmetic LIA verifier from previous work [PLDI 08] Benchmarks Strassen s 2x2 matrix multiplication R loop = * and R stack = 7 --- for holding the seven intermediate results Swapping two integers without a temporary R loop = * and R stack = 0 Computing the integral square root Linear search R loop = *; (*) and R stack = 1 Binary search R loop = *; (*) and R stack = 2 Discrete line drawing R loop = *; (*) and R stack = 1

Experiments: Predicate Abstraction Predicate abstraction verifier from previous work [PLDI 09] Benchmarks: Sorting Requires quantified specification and invariants E.g., All major sorting programs Specification: sortedness Vary resource constraints Nested loop, 0 extra variables: bubble sort, insertion sort Nested loop, 1 extra variable: selection sort Recursive, 0 extra variables: merge sort Recursive, 1 extra variable: quick sort Benchmarks: Dynamic Programming Iterative program from its recursive specification E.g., Fibonacci Specification f(0)=1, f(1)=1, k>2: f(k)=f(k-1)+f(k-2) R loop = *; (*) and R stack = 2 Generated program maintains sliding window (of size 2) and computes f(n)

Experiments: Synthesis times 10,000,000 1 around 10,000 seconds 1,000,000 8 under 1000 seconds 100,000 seconds (log scale) 10,000 8 under 10 seconds 1,000 0.1 100 Verification Synthesis 0.01 10 0.001 1 LIA verifier Predicate abstraction verifier

Summary: Proof-theoretic synthesis Proof-theoretic synthesis Synthesize programs and proof simultaneously Treat synthesis as generalized verification Principled approach to solving for programs using verification User input: scaffold Functional specification Space of desired program Domains of guards and statements Resource constraints Approach: One-shot synthesis, i.e., no iteration Constraints, synthesis conditions, encode the desired program Safety, termination, and well-formedness Solve using existing constraint-based verifiers Possible to synthesize wide variety of programs