Satisfiability Modulo Theories and its Applications in Program Verification and Synthesis

Satisfiability Modulo Theories and its Applications

in Program Verification and Synthesis

Iwo Błądek, Krzysztof Krawiec

Institute of Computing Science, Poznań University of Technology

Plan of the Presentation

1 Introduction

2 Satisfiability Modulo Theories (SMT)

3 SMT-Based Verification

4 SMT-Based Synthesis

5 Evolutionary Program Sketching

6 _Conclusions

Program

A sequence of instructions in a formal language, which may be executed on a dedicated machine.

x2+ x − 2

a ∨ b ∧ c bool isGreater(int x, int y) {

if (x > y ) return true; else return false; } false x = 1, y = 5 true x = 5, y = 1 1 a = 1, b = 0, c = 0 0 a = 0, b = 0, c = 0 0 x = 1 −2 x = 0

Program Synthesis

Aim of theprogram synthesis is to find a program given the desired

behavior of that program.

x2+ x − 2?

a ∨ b ∧ c?

bool isGreater(int x, int y) {

if (x > y ) return true; else return false; }

?

Program Specification

To describe the desired behavior of the program, a specification (intent)

is provided by a user. Two most commonly used types of specification are: Input-output examples. x y max(x,y) 0 0 0 1 0 1 3 4 4 · · · ·

Logical relations between input and output. max (x , y ) ≥ x ∧ max (x , y ) ≥ y ∧

General Workflow of Program Synthesis

Program Synthesis and Supervised Machine Learning

In the supervised machine learning we are interested in finding aclassifier

(or regressor), which can be thought of as a program in the traditional sense. Training set Classifier New data decision learning algorithm arguments

Program Synthesis and Supervised Machine Learning

Similarities:

Produced artifacts are programs (functions).

Results must be consistent with the data provided by a user. Differences:

Specification in program synthesis is assumed to be without errors/noise.

Machine learning is concerned with extracting knowledge and applying it to new examples, while program synthesis is rather concerned with discovering computational steps for known examples (specification). Generalization is not the main focus of program synthesis.

Approaches to Program Synthesis

The most popular approaches to program synthesis: Generate-and-Test

Exact search-space enumeration Heuristics, e.g. Genetic Programming

Automated deduction

Proofs-as-programs, e.g. SAT/SMT-based Program Synthesis Synthesis by transformations (specification rewriting)

Automated induction

Approaches to Program Synthesis

The most popular approaches to program synthesis: Generate-and-Test

Exact search-space enumeration Heuristics, e.g. Genetic Programming

Automated deduction

Proofs-as-programs, e.g. SAT/SMT-based Program Synthesis

Synthesis by transformations (specification rewriting)

Automated induction

Inductive Logic Programming

Plan of the Presentation

1 Introduction

2 Satisfiability Modulo Theories (SMT)

3 SMT-Based Verification

4 SMT-Based Synthesis

5 Evolutionary Program Sketching

Satisfiability Problem (SAT)

Question: Is the given formula in the propositional calculus satisfiable?

Examples: ¬a ∨ b

SAT: a = false, b = true

a ∧ ¬a ∧ b

UNSAT

Satisfiability Modulo Theories (SMT)

Satisfiability Modulo theories (SMT) is an area of

au-tomated deduction that studies methods for checking the

satisfiability of first-order formulas with respect to some

logical theory T of interest. It differs from general auto-mated deduction in that the background theory T need not be finitely or even first-order axiomatizable, and spe-cialized inference methods are used for each theory. By being theory-specific and restricting their language to cer-tain classes of formulas, these specialized methods can be implemented in solvers that are more efficient in practice than general-purpose theorem provers.

Satisfiability Modulo Theories (SMT)

Question: Is the given formula in the first-order logic satisfiable under the

specified background theory T , which defines semantics of a certain set of symbols?

Examples:

Logic: QF_LIA (Quantifier-Free Linear Integer Arithmetic) x , y , z ∈ Z a ∈ {false, true} (10 · x = 20) ∧ a SAT: x = 2, a = true (x < y ) ∧ (y < z) ∧ (z < x ) UNSAT (x ≤ y ) ∧ (y ≤ z) ∧ (z ≤ x ) SAT: x = 0, y = 0, z = 0

Satisfiability Modulo Theories (SMT)

Question: Is the given formula in the first-order logic satisfiable under the

specified background theory T , which defines semantics of a certain set of symbols?

Examples:

Logic: NIA (Non-Linear Integer Arithmetic) x , y ∈ Z

x2+ 1 ≤ 2 · x

SAT: x = 1

∀_{x ,y} (x + y )2> x2+ y2

SMT Solvers

SMT Solver – any software that can check satisfiability of formulas

modulo some given theory.

There are several freely accessible SMT solvers: CVC4 (open source)

MathSAT (free for non-commercial use)

Yices (open source, free for non-commercial use)

Z3, open source project of Microsoft Research (MIT license)

Most SMT solvers accept queries in the SMT-LIB language

(http://smtlib.cs.uiowa.edu/), which was created to standardize interaction with different solvers.

SMT Solvers

Plan of the Presentation

1 Introduction

2 Satisfiability Modulo Theories (SMT)

3 SMT-Based Verification

4 SMT-Based Synthesis

5 Evolutionary Program Sketching

6 _Conclusions

SMT-Based Program Verification

Program verification formula:

∃in,out ¬ (pre(in) ∧ program(in, out) =⇒ post(in, out))

where:

in – inputs to the program.

out – selected output variables (results) of the program.

pre(in) – precondition. Behavior of the program is specified only for inputs that satisfy pre(in).

program(in, out) –encoding of the program.

post(in, out) – postcondition. Describes expected behavior of the program.

SMT-Based Program Verification

SMT-based program verification is basically a search for counterexample. This is why the implication is negated. If verification returns UNSAT, then the program is correct.

An Example of SMT Verification

Task:

Synthesize a program max (x , y ) returning a maximum of two numbers.

max (x , y ) = ( x , if x ≥ y . y , otherwise. Formal specification: max (x , y ) ≥ x ∧ max (x , y ) ≥ y ∧ (max (x , y ) = x ∨ max (x , y ) = y )

An Example of SMT Verification

Program encoded as SMT formulas: ; PROGRAM (=> (< x y) (and (= res x) (= |res’’| res))) (=> (not (< x y)) (and (= |res’| y) (= |res’’| |res’|)))

An Example of SMT Verification

Verification constraints in SMT-LIB for the incorrect program: ; PRECONDITION

(assert true) ; PROGRAM

(assert (=> (< x y)

(and (= res x) (= |res’’| res))))

(assert (=> (not (< x y))

(and (= |res’| y) (= |res’’| |res’|)))) ; POSTCONDITION

(assert (not (and (>= |res’’| x) (>= |res’’| y) (or (= |res’’| x)

An Example of SMT Verification

This answer means that the program is not correct and solver provides us a counterexample.

An Example of SMT Verification

This answer means that the program is correct with respect to the specification. No counterexample was found.

Plan of the Presentation

1 Introduction

2 Satisfiability Modulo Theories (SMT)

3 SMT-Based Verification

4 SMT-Based Synthesis

5 Evolutionary Program Sketching

6 _Conclusions

Program Synthesis Formula

Program synthesis formula:

∃_svars∀_in,out pre(in) ∧ program(svars, in, out) =⇒ post(in, out)

where:

svars – structural variables, which determine the form of the synthesized program.

in – inputs to the program.

out – distinguished output variables (results) of the program.

pre(in) – precondition. Only for inputs satisfying the precondition behavior of the program is specified.

program(svars, in, out) – encoding of the program.

post(in, out) – postcondition. Describes expected behavior of the program.

An Example of SMT Synthesis

Task:

Synthesize a program max (x , y ) returning a maximum of two numbers.

max (x , y ) = ( x , if x ≥ y . y , otherwise. Formal specification: max (x , y ) ≥ x ∧ max (x , y ) ≥ y ∧ (max (x , y ) = x ∨ max (x , y ) = y )

An Example of SMT Synthesis

General structure of the solution (sketch), provided by a programmer:

if (H1): res = H2 else:

res = H3

H1, H2, H3 – holes to be filled by synthesizer.

This sketch, together with grammars describing holes contents, is translated to formulas in SMT-LIB language.

An Example of SMT Synthesis

Program’s encoding in the SMT-LIB language: (assert

(forall ((x Int)(y Int)(res Int)(|res’’| Int)(|res’| Int)) (=>

;PROGRAM:

(and

(=> (H1Start0 x y) ;TRUE IF BRANCH

(and (= res (H2Start0 x y)) (= |res’’| res))) (=> (not (H1Start0 x y)) ;ELSE IF BRANCH

(and (= |res’| (H3Start0 x y)) (= |res’’| |res’|))) )

;POSTCONDITION:

(and (>= |res’’| x) (>= |res’’| y) (or (= |res’’| x) (= |res’’| y))) )

))

An Example of SMT Synthesis

Encoding of holes grammars:

(define-fun H2Start0 ((x Int)(y Int)) Int

(ite (= H2Start0_r0 0) H2Start0_Int0 (ite (= H2Start0_r0 1) x (ite (= H2Start0_r0 2) y (ite (= H2Start0_r0 3) (+ x y) (ite (= H2Start0_r0 4) (- x y) ... )

An Example of SMT Synthesis

Model returned by SMT solver: (model

(define-fun H1Start0_Bool0 () Bool false) (define-fun H1Start0_r0 () Int 2)

(define-fun H1Start0_Int0 () Int (- 2))

(define-fun H2Start0_Int0 () Int 2)

(define-fun H2Start0_r0 () Int 1)

... )

Final synthesized code, created from model: if (>= x y):

res = x

else: res = y

Summary of SMT-Based Synthesis

Advantages:

Programs are guaranteed to be consistent with the specification for every input1.

For some problems, specification in the form of logical relations between input and output is more natural than in the form of a set of test cases.

Disadvantages:

Instructions of the program are limited by the theories accessible to the solver.

Size of the search space increases quickly with the number of instructions to be synthesized.

Undecidability of some theories leads to unknowns for harder instances.

1

Plan of the Presentation

1 Introduction

2 Satisfiability Modulo Theories (SMT)

3 SMT-Based Verification

4 SMT-Based Synthesis

5 Evolutionary Program Sketching

6 _Conclusions

Evolutionary Program Sketching

Our approach combining GP with SMT-based synthesis (currently submitted to EuroGP conference).

Sketching was proposed by Solar-Lezama [3] as a means of making formal synthesis feasible. One of it’s main characteristics was allowing holes in the partial program (sketch) to be filled by a synthesizer.

In our approach, human sketch-provider was replaced by an

evolutionary algorithm.

To this end, instruction set was extended with hole terminals, which were then filled by SMT solver (Z3).

Evolutionary Program Sketching

Some technical details

Query to the solver: maximize the number of passed test cases. Z3

offers some basic optimization functionality (faster than bisection-based multi-query alternative).

Evolutionary Program Sketching

Experiments

Configurations

Main configurations:

EPS-L (”Lamarckian” variant) holes permanently filled with content found by the solver; new holes introduced only by mutations.

EPS-B (”Baldwinian” variant) holes remain in programs after evaluation; solver only determines program’s fitness.

Combinations of available holes:

C (Constant holes) holes which could be filled with arbitrary

integer constant.

V (Variable holes) holes which could be filled with one of the

input variables.

CV (Constant and Variable holes) both C and V holes types

were available.

Experiments

Evolution parameters

Parameter Value

Population size 250

Maximum height of initial programs 4

Maximum height of subprograms inserted by mutation 4

Constant terminals (cs) drawn from interval [0, 5]

Maximum number of generations 100 100

Probability of mutation 0.5

Probability of crossover 0.5

Experiments

Benchmarks

Benchmarks were taken from the regression domain, but to make solver’s task easier all variable types and tests were switched to integers. NIA (Non-linear Integer Arithmetic) logic was used.

Benchmark #vars. Formula #tests

Keijzer12 2 x₁4− x3 1 + x22/2 − x2 49 Koza1 1 x 4_{+ x}3_{+ x}2_{+ x} 11 Koza1-p 3x4− 2x3_{+ 6x}2_{+ 3x − 4} Koza1-2D 2 x 4 1 + x23+ x12+ x2 49 Koza1-p-2D 3x₁4− 2x3 2 + 6x12+ 3x2− 4

Experiments

Results: number of optimal solutions found (/100)

EPS-L EPS-B GP GPT C V CV C V CV Keijzer12 0 0 0 0 1 39 1 0 Koza1 19 68 33 - 32 100 - 100 Koza1-p 0 0 5 - 3 100 - 100 Koza1-2D 1 12 2 0 11 80 21 23 Koza1-p-2D 0 0 0 0 1 75 0 0

GP standard GP running with the same iteration budget as EPS

configurations.

GPT standard GP running with the time budget equal to the

average time taken by all EPS configurations on the same benchmark.

Experiments

Results: end-of-run fitness

GP GPT EP S-LC EP S-LV EP S-LCV EP S-BC EP S-BV EP S-BCV 0 10 20 30 40 Fitness

Keijzer12(optimal fitness=49)

GP GPT EP S-LC EP S-LV EP S-LCV EP S-BC EP S-BV EP S-BCV 0 2 4 6 8 10 Fitness

Koza1(optimal fitness=11)

GP GPT EP S-LC EP S-LV EP S-LCV EP S-BC EP S-BV EP S-BCV 0 2 4 6 8 10 Fitness

Koza1-p(optimal fitness=11)

GP GPT EP S-LC EP S-LV EP S-LCV EP S-BC EP S-BV EP S-BCV 0 10 20 30 40 Fitness

Koza1-2D(optimal fitness=49)

GP GPT EP S-LC EP S-LV EP S-LCV EP S-BC EP S-BV EP S-BCV 0 10 20 30 40 Fitness

Koza1-p-2D(optimal fitness=49)

Experiments

Results: end-of-run fitness

GP GPT EP S-LC EP S-LV EP S-LCV EP S-BC EP S-BV EP S-BCV 0 10 20 30 40 Fitness

Keijzer12(optimal fitness=49)

GP GPT EP S-LC EP S-LV EP S-LCV EP S-BC EP S-BV EP S-BCV 0 2 4 6 8 10 Fitness

Koza1(optimal fitness=11)

GP GPT EP S-LC EP S-LV EP S-LCV EP S-BC EP S-BV EP S-BCV 0 2 4 6 8 10 Fitness

Koza1-p(optimal fitness=11)

GP GPT EP S-LC EP S-LV EP S-LCV EP S-BC EP S-BV EP S-BCV 0 10 20 30 40 Fitness

Koza1-2D(optimal fitness=49)

GP GPT EP S-LC EP S-LV EP S-LCV EP S-BC EP S-BV EP S-BCV 0 10 20 30 40 Fitness

Experiments

Results: average runtime [s]

EPS-L EPS-B GP GPT C V CV C V CV Keijzer12 15 11331 772 488 1579 15440 21173 28354 Koza1 5 291 670 - 801 652 - 696 Koza1-p 5 963 892 - 972 978 - 982 Koza1-2D 16 7636 793 479 1791 9077 16281 23034 Koza1-p-2D 15 9206 750 511 1726 11986 12391 27875

Experiments

Results: ratio of UNKNOWN solver response

EPS-L EPS-B C V CV C V CV Keijzer12 0.058 0.004 0.104 0.229 0.106 0.297 Koza1 0.080 - 0.058 0.127 - 0.120 Koza1-p 0.078 - 0.060 0.113 - 0.112 Koza1-2D 0.065 0.006 0.118 0.276 0.117 0.372 Koza1-p-2D 0.062 0.004 0.112 0.301 0.051 0.407

Plan of the Presentation

1 Introduction

2 Satisfiability Modulo Theories (SMT)

3 SMT-Based Verification

4 SMT-Based Synthesis

5 Evolutionary Program Sketching

6 _Conclusions

Future work

Continuation work:

Computational experiments on bigger number of benchmarks.

Different domains of benchmarks: Boolean, real numbered regression.

Different directions:

Bibliography I

[1] Sumit Gulwani.“Dimensions in Program Synthesis”. In: Proceedings of the 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming. PPDP ’10. Hagenberg, Austria: ACM, 2010, pp. 13–24.

[2] Sumit Gulwani et al. Component Based Synthesis Applied to

Bitvector Programs. Tech. rep. MSR-TR-2010-12. 2010.

[3] Armando Solar-Lezama. “Program Synthesis by Sketching”.

PhD thesis. USA: Electrical Engineering and Computer Science, University of California, Berkeley, 2008.

[4] Saurabh Srivastava, Sumit Gulwani, and Jeffrey S. Foster. “From

Program Verification to Program Synthesis”. In: Proceedings of the

37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL ’10. Madrid, Spain: ACM, 2010, pp. 313–326.