Constraint Solving andMachine Learning for Program
Verification and Synthesis
Hiroshi Unno
University of Tsukuba / RIKEN AIP
www.cs.tsukuba.ac.jp/~uhiro

Research Interests• Formal specification, verification, and synthesisof (mainly but not limited to) higher-order functional programs
by AI techniques such as constraint solving and machine learning• Ongoing projects• Synthesis of High-Level Programs from Temporal and Relational
Specifications (PI: Hiroshi Unno)• Program Verification Techniques for the AI Era(PI: Naoki Kobayashi)• AI Security and Privacy (PI: Jun Sakuma)• Metamathematics for Systems Design Project (PI: Ichiro Hasuo)• …
2020/12/18

STAIR Lab Software Technology Seminar2

This Talk
• Tutorial of program verification and synthesis basedon constraint solving and machine learning

2020/12/18

STAIR Lab Software Technology Seminar3

Background• Our society heavily relies on computer systems• Failure or malfunction of safety-critical systems would leadto human, social, economic, and environmental damage• 1985-1987 – Therac-25 medical accelerator delivered lethal
radiation doses to patients• June 4, 1996 – Ariane 5 Flight 501 exploded• February, 2014 – 1.9 million Prius cars recalled• April, 2014 – OpenSSL Heartbleed vulnerability disclosed• June 17, 2016 – Ethereum DAO attacked, over $55M stolen• Reliability assurance of safety-critical systems is crucial
2020/12/18

STAIR Lab Software Technology Seminar4

Program Verification• Formally prove or disprove a mathematical proposition 𝑄𝑄:“The given program satisfies its formal specification”• Great attentions from industry and academia• Microsoft’s SLAM & Everest projects, Facebook’s Infer, AWS• Turing awards to Hoare logic, temporal logic, model checking, …
Program & Spec.
let rec mc x =if x > 100 thenx – 10else
mc (mc (x + 11))in
let n = randi() in
if n ≤ 101 thenassert (mc n = 91)
2020/12/18

Program Verifier
STAIR Lab Software Technology Seminar

A proof of 𝑄𝑄
or
A counterexample to 𝑄𝑄(e.g., a program input
leading to a spec. violation)or
Unknown5

Program Synthesis• Input an incomplete program and its specification 𝝓𝝓,and output an executable program 𝑷𝑷 that satisfies 𝝓𝝓• 𝜙𝜙 specifies extensional (what 𝑃𝑃 computes) and/or
intentional (how 𝑃𝑃 computes) behaviors of 𝑃𝑃• 𝜙𝜙 is represented as a logical formula, input/output examples(e.g., MS Excel FlashFill), a natural language sentence, …

A program satisfying the spec.
let rec mc x =if x > 100 thenx – 10else
mc (mc (x + 11))

Incomplete Program& Specification
let rec mc x = ?
let n = randi() in
if n ≤ 101 thenassert (mc n = 91)
2020/12/18

Program Synthesizer
STAIR Lab Software Technology Seminaror
A proof of unrealizabilityorUnknown
6

Enabling Technologies• Program logics for mechanizing verification & synthesis• Hoare logic for proving Hoare triples 𝑃𝑃 𝑐𝑐 𝑄𝑄 meaning that:

For any initial state 𝜎𝜎 that satisfies the precondition 𝑃𝑃, if the executionof the program 𝑐𝑐 under 𝜎𝜎 terminates, the postcondition 𝑄𝑄 is satisfied by
the resulting state• Separation logic• Dependent refinement type system• Graded modal type system• Constraint solvers for automating verification & synthesis• SAT solvers: satisfiability checker for propositional formulas• SMT solvers: satisfiability checker for predicate formulas overfirst-order theories on integers, reals, lists, arrays, …

What about functions (that represent inductive invariants,
rankingfunctions, recurrent
sets,Seminar
Skolem functions, …)?
2020/12/18
STAIR Lab Software Technology
7This Talk
• Tutorial of program verification and synthesis based on
constraint solving and machine learning over functions• First part: How to reduce program verification andsynthesis to constraint solving• Second part: How to solve constraints via integrated
deductive and inductive reasoning• Deductive reasoning by theorem proving (e.g., SAT, SMT)
• Inductive reasoning by machine learning (e.g., decision tree
learning, reinforcement learning)
2020/12/18

STAIR Lab Software Technology Seminar

8

This Talk
• Tutorial of program verification and synthesis based on
constraint solving and machine learning over functions• First part: How to reduce program verification andsynthesis to constraint solving• Second part: How to solve constraints via integrated
deductive and inductive reasoning• Deductive reasoning by theorem proving (e.g., SAT, SMT)
• Inductive reasoning by machine learning (e.g., decision tree
learning, reinforcement learning)
2020/12/18

STAIR Lab Software Technology Seminar9

Program Verification via
Constraint Solving
Target Program 𝑷𝑷 & Specification 𝝍𝝍Constraint
Generation

Constraints 𝓒𝓒 on Function Variables

Verification Intermediary
Independent of Particular
Target and Method 2020/12/18

Constraint
Solving

𝓒𝓒 is Sat (𝑷𝑷 satisfies 𝝍𝝍),𝓒𝓒 is Unsat (𝑷𝑷 violates 𝝍𝝍),or Unknown
STAIR Lab Software Technology Seminar

10

Program Verification via
Constrained Horn Clauses (CHCs)
Target Program 𝑷𝑷 & Specification 𝝍𝝍Constraint
Generation

JayHorn for Java [Kahsai+ ’16]
SeaHorn for C [Gurfinkel+ ’15]
RCaml for OCaml [Unno+ ’09]

CHCs Constraints 𝓒𝓒 on Predicate Variables
Constraint
Solving

2020/12/18

SPACER [Komuravelli+ ’14]
Hoice [Champion+ ’18]
Eldarica [Hojjat+ ’18]

𝓒𝓒 is Sat (𝑷𝑷 satisfies 𝝍𝝍),𝓒𝓒 is Unsat (𝑷𝑷 violates 𝝍𝝍),or Unknown
STAIR Lab Software Technology Seminar

11

CHCs: Constrained Horn Clauses(see e.g., [Bjørner+ ’15] )• A finite set 𝓒𝓒 of Horn-clauses of either form:

𝑋𝑋0 𝑡𝑡�0 ⟸ 𝑋𝑋1 𝑡𝑡�1 ∧ ⋯ ∧ 𝑋𝑋𝑚𝑚 𝑡𝑡�
𝑚𝑚 ∧ 𝜙𝜙or ⊥ ⟸ 𝑋𝑋 𝑡𝑡� ∧ ⋯ ∧ 𝑋𝑋
1 1
𝑚𝑚 𝑡𝑡�
𝑚𝑚 ∧ 𝜙𝜙

where 𝑋𝑋0 , 𝑋𝑋1 … , 𝑋𝑋𝑚𝑚 are predicate variables,
st-order theory 𝑇𝑇,
aresequences
of
terms
of
a
1
𝑡𝑡�0 , … , 𝑡𝑡�
𝑚𝑚
𝜙𝜙 is a formula of 𝑇𝑇 without predicate variables.

• 𝓒𝓒 is satisfiable (modulo 𝑇𝑇) if there is an interpretation 𝜌𝜌 ofpredicate variables such that 𝜌𝜌 ⊨ ⋀𝓒𝓒
2020/12/18

STAIR Lab Software Technology Seminar

12

Prog. & Spec.

SAT or UNSAT

CHCs

Constraint Generation

Constraint Solving

Example Program and Partial Correctness Specification:
Precondition

Postcondition

2020/12/18

𝑥𝑥 = 𝑥𝑥0
𝑦𝑦 = 0;
𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝑥𝑥 ≠ 0 𝐝𝐝𝐝𝐝
𝑦𝑦 ← 𝑦𝑦 + 1;
𝑥𝑥 ← 𝑥𝑥 − 1
𝐝𝐝𝐝𝐝𝐝𝐝𝐝𝐝
𝑦𝑦 = 𝑥𝑥0

If the initial state satisfies
the pre-condition 𝑥𝑥 = 𝑥𝑥0
and the loop terminates

the post-condition 𝑦𝑦 = 𝑥𝑥0 is
satisfied by the resulting state

STAIR Lab Software Technology Seminar13

Prog. & Spec.
Constraint Generation

Input:

Output 𝓒𝓒:

𝑥𝑥 = 𝑥𝑥0①
𝑦𝑦 = 0;②
𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝑥𝑥 ≠ 0 𝐝𝐝𝐝𝐝
𝑦𝑦 ← 𝑦𝑦 + 1;
𝑥𝑥 ← 𝑥𝑥 − 1③
𝐝𝐝𝐝𝐝𝐝𝐝𝐝𝐝
𝑦𝑦 = 𝑥𝑥0
2020/12/18

SAT or UNSAT

CHCs

Constraint Solving

represents a loop invariant

𝐼𝐼 𝑥𝑥0 , 𝑥𝑥, 𝑦𝑦 ⟸ 𝑥𝑥 = 𝑥𝑥0 ∧ 𝑦𝑦 = 0 ,𝐼𝐼 𝑥𝑥0 , 𝑥𝑥 − 1, 𝑦𝑦 + 1⟸ 𝐼𝐼 𝑥𝑥0 , 𝑥𝑥, 𝑦𝑦 ∧ 𝑥𝑥 ≠ 0,
𝑦𝑦 = 𝑥𝑥0 ⟸ 𝐼𝐼 𝑥𝑥0 , 𝑥𝑥, 𝑦𝑦 ∧ 𝑥𝑥 = 0

𝓒𝓒 is satisfiable, witnessed by asolution 𝐼𝐼 𝑥𝑥0 , 𝑥𝑥, 𝑦𝑦 ≡ 𝑥𝑥0 = 𝑥𝑥 + 𝑦𝑦

STAIR Lab Software Technology Seminar

14

Program Verification via
Constrained Horn Clauses (CHCs)
Target Program 𝑷𝑷 & Specification 𝝍𝝍Limited to Linear-Time
Safety Verification Constraint
Generation

CHCs Constraints 𝓒𝓒 on Predicate Variables
Constraint
Solving

2020/12/18

𝓒𝓒 is Sat (𝑷𝑷 satisfies 𝝍𝝍),𝓒𝓒 is Unsat (𝑷𝑷 violates 𝝍𝝍),or Unknown
STAIR Lab Software Technology Seminar

15

Program Verification via Predicate
Constraint Satisfaction [Satake+ ’20]
Target Program 𝑷𝑷 & Specification 𝝍𝝍

Applicable to (Finitely-)Branching-Time Safety
Verification Constraint
Generation

pCSP Constraints 𝓒𝓒 on Predicate Variables
Constraint
Solving

2020/12/18

PCSat [Satake+ ’20, Unno+ ’20]

𝓒𝓒 is Sat (𝑷𝑷 satisfies 𝝍𝝍),𝓒𝓒 is Unsat (𝑷𝑷 violates 𝝍𝝍),or Unknown
STAIR Lab Software Technology Seminar

16

Linear-Time vs. Branching-Time
Verification of Non-det. Programs• The target program 𝑷𝑷 may exhibit non-determinism
caused by user input, network comm., scheduling, …
• Linear-time verification concerns properties ofthe execution traces of 𝑷𝑷• Branching-time verification concerns properties of thecomputation tree of 𝑷𝑷• Subsumes linear-time verification• Example: Non-termination verification of deciding whether
there is an infinite execution of 𝑷𝑷(cf. termination verification decides whether all execution of
𝑷𝑷 is finite)

2020/12/18

STAIR Lab Software Technology Seminar

17

pCSP: Predicate Constraint
Satisfaction Problem [Satake+ ’20]
• A finite set 𝓒𝓒 of clauses of the form:

𝑋𝑋1 𝑡𝑡�1 ∨ ⋯ ∨ 𝑋𝑋ℓ 𝑡𝑡�ℓ ⟸� ∧ ⋯ ∧ 𝑋𝑋𝑚𝑚 𝑡𝑡�
𝑋𝑋ℓ+1 𝑡𝑡ℓ+1
𝑚𝑚 ∧ 𝜙𝜙

where 𝑋𝑋1 , … , 𝑋𝑋𝑚𝑚 are predicate variables,st𝑡𝑡�1 , … , 𝑡𝑡�
𝑚𝑚 are sequences of terms of a 1 -order theory 𝑇𝑇,
𝜙𝜙 is a formula of 𝑇𝑇 without predicate variables.

• 𝓒𝓒 is satisfiable (modulo 𝑇𝑇) if there is an interpretation 𝜌𝜌 ofpredicate variables such that 𝜌𝜌 ⊨ ⋀𝓒𝓒• 𝓒𝓒 is CHCs if ℓ ≤ 1 for all clause in 𝓒𝓒
2020/12/18

STAIR Lab Software Technology Seminar18

Prog. & Spec.

Constraint Generation

Example Program and Specification:
Precondition𝑥𝑥 > 0
𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝑥𝑥 ≠ 0 𝐝𝐝𝐝𝐝
Non-det.
𝐢𝐢𝐢𝐢 𝐫𝐫𝐫𝐫𝐫𝐫𝐫𝐫_𝐛𝐛𝐛𝐛𝐛𝐛𝐛𝐛
branching𝑥𝑥 ← 𝑥𝑥 − 1𝐞𝐞𝐞𝐞𝐞𝐞𝐞𝐞𝑥𝑥 ← 𝑥𝑥 + 1
𝐝𝐝𝐝𝐝𝐝𝐝𝐝𝐝
Post⊥ Contradiction
condition
2020/12/18

SAT or UNSAT

pCSP∃ 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭

Constraint Solving

If the initial state satisfies
the pre-condition 𝑥𝑥 > 0

there is an execution of
the program such thatthe post-condition ⊥ issatisfied when the while
loop terminates

STAIR Lab Software Technology Seminar

19

Prog. & Spec.

Constraint Generation

Example Program and Specification:
Precondition𝑥𝑥 > 0
𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝑥𝑥 ≠ 0 𝐝𝐝𝐝𝐝
Non-det.
𝐢𝐢𝐢𝐢 𝐫𝐫𝐫𝐫𝐫𝐫𝐫𝐫_𝐛𝐛𝐛𝐛𝐛𝐛𝐛𝐛
branching𝑥𝑥 ← 𝑥𝑥 − 1𝐞𝐞𝐞𝐞𝐞𝐞𝐞𝐞𝑥𝑥 ← 𝑥𝑥 + 1
𝐝𝐝𝐝𝐝𝐝𝐝𝐝𝐝
Post⊥ Contradiction
condition
2020/12/18

SAT or UNSAT

pCSP∃ 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭

Constraint Solving

If the initial state satisfies
the pre-condition 𝑥𝑥 > 0

STAIR Lab Software Technology Seminar

there is an execution of
the program such thatthe while loop
never terminates
20Prog. & Spec.

pCSP

Constraint Generation

Input:
𝑥𝑥 > 0
𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝑥𝑥 ≠ 0 𝐝𝐝𝐝𝐝𝐢𝐢𝐢𝐢 𝐫𝐫𝐫𝐫𝐫𝐫𝐫𝐫_𝐛𝐛𝐛𝐛𝐛𝐛𝐛𝐛
𝑥𝑥 ← 𝑥𝑥 − 1𝐞𝐞𝐞𝐞𝐞𝐞𝐞𝐞𝑥𝑥 ← 𝑥𝑥 + 1
𝐝𝐝𝐝𝐝𝐝𝐝𝐝𝐝⊥
2020/12/18

SAT or UNSAT
Constraint Solving

represents a loop invariant
preserved by some execution
Output 𝓒𝓒:(i.e., recurrent set)

① 𝐼𝐼 𝑥𝑥 ⟸ 𝑥𝑥 > 0,
∃ 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭② 𝐼𝐼 𝑥𝑥 − 1 ∨ 𝐼𝐼 𝑥𝑥 + 1
𝓒𝓒 is beyond⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 ≠ 0,CHCs!
③ ⊥ ⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 = 0
𝓒𝓒 is satisfiable, witnessed by≡ 𝑥𝑥 > 0 21
aTechnology
solution
STAIR Lab Software
Seminar 𝐼𝐼 𝑥𝑥

Program Verification via Extended
Predicate Constraint Satisfaction [Unno+ ’20]
Target Program 𝑷𝑷 & Specification 𝝍𝝍

Applicable to (Infinitely-)Branching-Time Safety &Liveness Verification Constraint
Generation

pfwCSP Constraints 𝓒𝓒 on Predicate Variables
Constraint
Solving

2020/12/18

PCSat [Satake+ ’20, Unno+ ’20]

𝓒𝓒 is Sat (𝑷𝑷 satisfies 𝝍𝝍),𝓒𝓒 is Unsat (𝑷𝑷 violates 𝝍𝝍),or Unknown
STAIR Lab Software Technology Seminar

22

Safety vs. Liveness Verification• Safety is a class of properties of the form
“something bad will never happen”• Examples (absence of): assertion failure, division-by-zero,array boundary violation, …

• Liveness is a class of properties of the form
“something good will eventually happen”• Examples: termination, deadlock freedom, …

2020/12/18

STAIR Lab Software Technology Seminar

23

pfwCSP: Extension of pCSP with Functionaland Well-founded Predicates [Unno+ ’20]
(cf. ∀∃CHCs with dwf [Beyene+ ’13])• A finite set 𝓒𝓒 of pCSP clauses equipped witha map 𝓚𝓚 from predicate variable 𝑋𝑋 in 𝓒𝓒 to ⋆, 𝜆𝜆, ⇓• 𝑋𝑋 is ordinary predicate if 𝓚𝓚 𝑋𝑋 = ⋆• 𝑋𝑋 is functional predicate if 𝓚𝓚 𝑋𝑋 = 𝜆𝜆• 𝑋𝑋 is well-founded predicate if 𝓚𝓚 𝑋𝑋 = ⇓• 𝓒𝓒 is satisfiable (modulo 𝑇𝑇) if there is an interpretation𝜌𝜌 of predicate variables such that• 𝜌𝜌 ⊨ ⋀𝓒𝓒• ∀𝑋𝑋. 𝓚𝓚 𝑋𝑋 = 𝜆𝜆 ⟹ 𝜌𝜌 𝑋𝑋 characterizes a total function• ∀𝑋𝑋. 𝓚𝓚 𝑋𝑋 = ⇓ ⟹ 𝜌𝜌 𝑋𝑋 represents a well-founded relation

2020/12/18

STAIR Lab Software Technology Seminar24

Prog. & Spec.

SAT or UNSAT

pfwCSP

Constraint Generation

Constraint Solving

Example Program and Specification:
Precondition
Non-det.
integer
Postcondition𝑥𝑥 > 0
𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝑥𝑥 > 0 𝐝𝐝𝐝𝐝𝑥𝑥 ← 𝐫𝐫𝐫𝐫𝐫𝐫𝐫𝐫_𝐢𝐢𝐢𝐢𝐢𝐢
𝐝𝐝𝐝𝐝𝐝𝐝𝐝𝐝⊥
Contradiction

2020/12/18

∃

− 𝑥𝑥

If the initial state satisfies
the pre-condition 𝑥𝑥 > 0

STAIR Lab Software Technology Seminar

there is an execution of
the program such thatthe while loop
never terminates
25

Prog. & Spec.

pfwCSP

Constraint Generation

SAT or UNSAT

Constraint Solving

represents a loop invariant
preserved by some execution
Output 𝓒𝓒:(i.e., recurrent set)

Input:

𝑥𝑥 > 0①
𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝑥𝑥 > 0 𝐝𝐝𝐝𝐝𝑥𝑥 ← 𝐫𝐫𝐫𝐫𝐫𝐫𝐫𝐫_𝐢𝐢𝐢𝐢𝐢𝐢 ∃ − 𝑥𝑥 ②
𝐝𝐝𝐝𝐝𝐝𝐝𝐝𝐝 𝓒𝓒 is beyond pCSP but canbe encoded in pfwCSP⊥

𝐼𝐼 𝑥𝑥 ⟸ 𝑥𝑥 > 0,

∃𝑟𝑟. 𝐼𝐼 𝑟𝑟 − 𝑥𝑥
⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 > 0,
using a functional pred.
③ ⊥ ⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 ≤ 0var. that characterizes
a Skolem function for 𝒓𝒓

2020/12/18

STAIR Lab Software Technology Seminar

26

Prog. & Spec.

pfwCSP

Constraint Generation

Input:
𝑥𝑥 > 0
𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝑥𝑥 > 0 𝐝𝐝𝐝𝐝𝑥𝑥 ← 𝐫𝐫𝐫𝐫𝐫𝐫𝐫𝐫_𝐢𝐢𝐢𝐢𝐢𝐢
𝐝𝐝𝐝𝐝𝐝𝐝𝐝𝐝⊥
2020/12/18

Output 𝓒𝓒:

SAT or UNSAT

Constraint Solving

characterizes a Skolem
function mapping 𝑥𝑥 to 𝑟𝑟① 𝐼𝐼 𝑥𝑥 ⟸ 𝑥𝑥 > 0,
②
𝐼𝐼
𝑟𝑟
−
𝑥𝑥
⟸
𝑆𝑆
𝑥𝑥,
𝑟𝑟
𝜆𝜆
∃
− 𝑥𝑥
∧ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 > 0,
③ ⊥ ⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 ≤ 0

𝓒𝓒 is satisfiable, witnessed by a solution
𝑥𝑥 Lab≡𝑥𝑥 > 0, 𝑆𝑆𝜆𝜆 𝑥𝑥, 𝑟𝑟 ≡ 𝑟𝑟 = 𝑥𝑥 + 127
𝐼𝐼STAIR
Software Technology SeminarProg. & Spec.

pfwCSP

Constraint Generation

SAT or UNSAT

Constraint Solving

Example Program and Total Correctness Specification:
Precondition

Postcondition
2020/12/18

𝑥𝑥 ≠ 0
𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝑥𝑥 ≠ 0 𝐝𝐝𝐝𝐝𝐢𝐢𝐢𝐢 𝑥𝑥 > 0 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭
𝑥𝑥 ← 𝑥𝑥 − 1𝐞𝐞𝐞𝐞𝐞𝐞𝐞𝐞𝑥𝑥 ← 𝑥𝑥 + 1
𝐝𝐝𝐝𝐝𝐝𝐝𝐝𝐝⊤
Tautology

If the initial state satisfies
the pre-condition 𝑥𝑥 ≠ 0

the loop always terminates
and the post-condition ⊤ issatisfied by the resulting state

STAIR Lab Software Technology Seminar28

Prog. & Spec.

pfwCSP

Constraint Generation

Input:

Output 𝓒𝓒:

SAT or UNSAT

Constraint Solving

represents a loop invariant

𝑥𝑥 ≠ 0① 𝐼𝐼 𝑥𝑥 ⟸ 𝑥𝑥 = 0,
𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝑥𝑥 ≠ 0 𝐝𝐝𝐝𝐝𝐢𝐢𝐢𝐢 𝑥𝑥 > 0 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 ② 𝐼𝐼 𝑥𝑥 − 1 ⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 > 0,𝑥𝑥 ← 𝑥𝑥 − 1
③
𝐼𝐼
𝑥𝑥
+
1
⟸
𝐼𝐼
𝑥𝑥
∧
𝑥𝑥
<
0,
𝐞𝐞𝐞𝐞𝐞𝐞𝐞𝐞𝑥𝑥 ← 𝑥𝑥 + 1 ④ 𝑇𝑇⇓ 𝑥𝑥, 𝑥𝑥 − 1 ⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 > 0,
𝐝𝐝𝐝𝐝𝐝𝐝𝐝𝐝
⑤
𝑇𝑇
𝑥𝑥,
𝑥𝑥
+
1
⟸
𝐼𝐼
𝑥𝑥
∧
𝑥𝑥
<
0,
⇓
⊤
represents a wellfounded relation for 𝓒𝓒 is satisfiable, witnessed by a solution
terminationof the loop 𝐼𝐼STAIR𝑥𝑥Lab Software
2020/12/18
Seminar≡ ⊤,Technology
𝑇𝑇 𝑥𝑥,
𝑥𝑥𝑥 ≡ 𝑥𝑥 > 𝑥𝑥 ′ ≥290⇓

Further Applications of pfwCSP• Refinement type inference [Unno+ ’09,’13,’18, Nanjo’18, Katsura+ ’20]
• Validity checking of fixpoint logic formulas• LTL, CTL, CTL*, modal-mu calculus model checking• Infinite-state infinite-duration game solving• Bisimulation and bisimilarity verification• Hyperproperties verification• Program synthesis•…
2020/12/18(see [Unno+ ’20] and upcoming papers)
STAIR Lab Software Technology Seminar

30

Program Synthesis via
Constraint Solving
Language 𝓛𝓛 & Specification 𝝍𝝍Constraint
Generation

Constraints 𝓒𝓒 on Function Variables

Synthesis Intermediary
Independent of Particular
Target and Method 2020/12/18

Constraint
Solving

𝓒𝓒 is Sat (some 𝑷𝑷 ∈ 𝓛𝓛 satisfies 𝝍𝝍),𝓒𝓒 is Unsat (all 𝑷𝑷 ∈ 𝓛𝓛 violates 𝝍𝝍),or Unknown
STAIR Lab Software Technology Seminar

31

Program Synthesis via
Syntax-Guided Synthesis (SyGuS)
Language 𝓛𝓛 & Specification 𝝍𝝍Constraint
Generation

SyGuS Constraints 𝓒𝓒 on Function Variables
Constraint
Solving

2020/12/18

CVC4 [Reynolds+ ’15,’19]
DryadSynth [Huang+ ’20]
PCSat [Satake+ ’20, Unno+ ’20]

𝓒𝓒 is Sat (some 𝑷𝑷 ∈ 𝓛𝓛 satisfies 𝝍𝝍),𝓒𝓒 is Unsat (all 𝑷𝑷 ∈ 𝓛𝓛 violates 𝝍𝝍),or Unknown
STAIR Lab Software Technology Seminar

32

SyGuS: Syntax-Guided
Synthesis [Alur+ ’15]
• Fix a first-order background theory 𝑇𝑇 such as:• Linear integer arithmetic (LIA)• Strings (for FlashFill benchmarks)• Bit-vectors (for Hackers' Delight benchmarks)• Given• Specification: 𝑇𝑇-formula 𝜙𝜙 over a function variable 𝑓𝑓• Language: context-free grammar 𝐺𝐺 characterizing theset ℒ 𝐺𝐺 of allowed 𝑇𝑇-terms• Find a term 𝑡𝑡 ∈ ℒ 𝐺𝐺 such that ⊨ 𝑡𝑡/𝑓𝑓 𝜙𝜙2020/12/18

STAIR Lab Software Technology Seminar

33

Example LIA SyGuS Constraints 𝓒𝓒:• Language: 𝐺𝐺 that generates any term of LIA

𝑓𝑓 𝑥𝑥, 𝑦𝑦 ≥ 𝑥𝑥 ∧ 𝑓𝑓 𝑥𝑥, 𝑦𝑦 ≥ 𝑦𝑦 ∧• Specification: 𝜙𝜙 ≡𝑓𝑓 𝑥𝑥, 𝑦𝑦 = 𝑥𝑥 ∨ 𝑓𝑓 𝑥𝑥, 𝑦𝑦 = 𝑦𝑦

𝓒𝓒 is satisfied by 𝑓𝑓 𝑥𝑥, 𝑦𝑦 ≡ if 𝑥𝑥 > 𝑦𝑦 then 𝑥𝑥 else 𝑦𝑦

𝓒𝓒 can be reduced to the pfwCSP:
𝑟𝑟 ≥ 𝑥𝑥 ∧ 𝑟𝑟 ≥ 𝑦𝑦 ∧ 𝑟𝑟 = 𝑥𝑥 ∨ 𝑟𝑟 = 𝑦𝑦 ⟸ 𝐹𝐹𝜆𝜆 𝑥𝑥, 𝑦𝑦, 𝑟𝑟

In general, SyGuS constraints 𝓒𝓒 can be converted toa pfwCSP using a predicate that characterizes ℒ 𝐺𝐺
2020/12/18

STAIR Lab Software Technology Seminar

34

This Talk
• Tutorial of program verification and synthesis based on
constraint solving and machine learning over functions• First part: How to reduce program verification andsynthesis to constraint solving• Second part: How to solve constraints via integrated
deductive and inductive reasoning• Deductive reasoning by theorem proving (e.g., SAT, SMT)
• Inductive reasoning by machine learning (e.g., decision tree
learning, reinforcement learning)
2020/12/18

STAIR Lab Software Technology Seminar

35

Program Verification and Synthesis via
Predicate Constraint Satisfaction
Target Program 𝑷𝑷 &Specification 𝝍𝝍Constraint
Generation

Language 𝓛𝓛 &Specification 𝝍𝝍

pfwCSP Constraints 𝓒𝓒 on Predicate Variables
Constraint
Solving

2020/12/18

𝓒𝓒 is Sat, 𝓒𝓒 is Unsat, or Unknown
STAIR Lab Software Technology Seminar

36Challenges in Constraint Solving• Undecidable in general even for decidable theories• The search space of solutions is often very large(or unbounded), high-dimensional, and non-smooth

To address these challenges, researchers areintegrating deductive & inductive reasoning
techniques within the framework ofCounterExample Guided Inductive Synthesis(CEGIS) [Solar-Lezama+ ’06]
2020/12/18

STAIR Lab Software Technology Seminar

37

CounterExample Guided
Inductive Synthesis (CEGIS)• Iteratively accumulate example instances 𝓔𝓔 of thegiven 𝓒𝓒 through the two phases for each iteration:• Synthesis Phase by Learner• Find a candidate solution 𝜌𝜌 that satisfies 𝓔𝓔• Validation Phase by Teacher• Check if the candidate 𝜌𝜌 also satisfies 𝓒𝓒 (with an SMT solver)• If yes, return 𝜌𝜌 as a genuine solution of 𝓒𝓒• If no, repeat the procedure with new example instances
witnessing non-satisfaction of 𝓒𝓒 by 𝜌𝜌 added

2020/12/18

STAIR Lab Software Technology Seminar

38

Example Run of CEGIS
Learner

Teacher

Example Instances 𝓔𝓔:

Constraints 𝓒𝓒:∅

Starting fromthe empty set(𝓒𝓒 is a black box)

2020/12/18• 𝐼𝐼 𝑥𝑥 ⟸ 𝑥𝑥 > 0• 𝐼𝐼 𝑥𝑥 − 1 ∨ 𝐼𝐼 𝑥𝑥 + 1⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 ≠ 0• ⊥ ⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 = 0

Is the candidate 𝐼𝐼 𝑥𝑥 ↦ ⊤ genuine?
STAIR Lab Software Technology Seminar

39

Example Run of CEGIS
Learner

Teacher

Example Instances 𝓔𝓔:

Constraints 𝓒𝓒:⊥ ⟸ 𝐼𝐼 0∅ ∧ 0 = 0• 𝐼𝐼 𝑥𝑥 ⟸ 𝑥𝑥 > 0• 𝐼𝐼 𝑥𝑥 − 1 ∨ 𝐼𝐼 𝑥𝑥 + 1⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 ≠ 0• ⊥ ⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 = 0

2020/12/18

No. 𝐼𝐼 𝑥𝑥 ↦ ⊤ is not.
The 3rd clause is violated when 𝑥𝑥 = 0
STAIR Lab Software Technology Seminar

40

Example Run of CEGIS
Learner

Teacher

Example Instances 𝓔𝓔:

Constraints 𝓒𝓒:¬𝐼𝐼 0• 𝐼𝐼 𝑥𝑥 ⟸ 𝑥𝑥 > 0• 𝐼𝐼 𝑥𝑥 − 1 ∨ 𝐼𝐼 𝑥𝑥 + 1⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 ≠ 0• ⊥ ⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 = 0

2020/12/18

Is the cand. 𝐼𝐼 𝑥𝑥 ↦ 𝑥𝑥 < 0 genuine?
STAIR Lab Software Technology Seminar

41

Example Run of CEGIS
Learner

Teacher

Example Instances 𝓔𝓔:

Constraints 𝓒𝓒:¬𝐼𝐼 0

𝐼𝐼 1 ⟸ 1 > 0

2020/12/18• 𝐼𝐼 𝑥𝑥 ⟸ 𝑥𝑥 > 0• 𝐼𝐼 𝑥𝑥 − 1 ∨ 𝐼𝐼 𝑥𝑥 + 1⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 ≠ 0• ⊥ ⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 = 0

No. 𝐼𝐼 𝑥𝑥 ↦ 𝑥𝑥 < 0 is not.
The 1st clause is violated when 𝑥𝑥 = 1
STAIR Lab Software Technology Seminar

42

Example Run of CEGIS
Learner

Teacher

Example Instances 𝓔𝓔:

Constraints 𝓒𝓒:

¬𝐼𝐼 0
𝐼𝐼 1

2020/12/18• 𝐼𝐼 𝑥𝑥 ⟸ 𝑥𝑥 > 0• 𝐼𝐼 𝑥𝑥 − 1 ∨ 𝐼𝐼 𝑥𝑥 + 1⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 ≠ 0• ⊥ ⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 = 0

Is the cand. 𝐼𝐼 𝑥𝑥 ↦ 𝑥𝑥 = 1 genuine?
STAIR Lab Software Technology Seminar

43

Example Run of CEGIS
Learner

Teacher

Example Instances 𝓔𝓔:

Constraints 𝓒𝓒:¬𝐼𝐼 0
𝐼𝐼 0 ∨ 𝐼𝐼 2 ⟸ 𝐼𝐼 1
𝐼𝐼 1

2020/12/18• 𝐼𝐼 𝑥𝑥 ⟸ 𝑥𝑥 > 0• 𝐼𝐼 𝑥𝑥 − 1 ∨ 𝐼𝐼 𝑥𝑥 + 1⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 ≠ 0• ⊥ ⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 = 0

No. 𝐼𝐼 𝑥𝑥 ↦ 𝑥𝑥 = 1 is not.
The 2nd clause is violated when 𝑥𝑥 = 1
STAIR Lab Software Technology Seminar

44

Example Run of CEGIS
Learner

Teacher

Example Instances 𝓔𝓔:

Constraints 𝓒𝓒:¬𝐼𝐼 0
𝐼𝐼 0 ∨ 𝐼𝐼 2 ⟸ 𝐼𝐼 1
𝐼𝐼 1

2020/12/18• 𝐼𝐼 𝑥𝑥 ⟸ 𝑥𝑥 > 0• 𝐼𝐼 𝑥𝑥 − 1 ∨ 𝐼𝐼 𝑥𝑥 + 1⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 ≠ 0• ⊥ ⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 = 0

Is the cand. 𝐼𝐼 𝑥𝑥 ↦ 𝑥𝑥 ≥ 1 genuine?
STAIR Lab Software Technology Seminar

45

Example Run of CEGIS
Learner

Teacher

Example Instances 𝓔𝓔:

Constraints 𝓒𝓒:¬𝐼𝐼 0
𝐼𝐼 0 ∨ 𝐼𝐼 2 ⟸ 𝐼𝐼 1
𝐼𝐼 1

2020/12/18• 𝐼𝐼 𝑥𝑥 ⟸ 𝑥𝑥 > 0• 𝐼𝐼 𝑥𝑥 − 1 ∨ 𝐼𝐼 𝑥𝑥 + 1⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 ≠ 0• ⊥ ⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 = 0

Yes. 𝐼𝐼 𝑥𝑥 ↦ 𝑥𝑥 ≥ 1 satisfies 𝓒𝓒!
STAIR Lab Software Technology Seminar46

Is CEGIS just (Online) Supervised
Learning of Classification?
• Similarities• Learner trains a model to fit examples 𝓔𝓔 and obtain 𝜌𝜌• Teacher requires 𝜌𝜌 to generalize to 𝓒𝓒 (𝜌𝜌 shouldn’t overfit 𝓔𝓔)• Differences• 𝓔𝓔 is usually assumed to have no noise & 𝓒𝓒 is hard constraints• 𝜌𝜌 is required to exactly satisfy 𝓔𝓔 (or has no chance to satisfy 𝓒𝓒)• 𝜌𝜌 should be efficiently handled by Teacher (i.e., an SMT solver)• Sampling of 𝓔𝓔 from 𝓒𝓒 is not i.i.d (depends on 𝜌𝜌 and Teacher)• 𝓔𝓔 may contain not only positive/negative examples but also
arbitrary clause ones (cf. constrained semi-supervised learning)

Despite the differences, machine learning
out
to be
quite useful!
2020/12/18 techniques turned
STAIR Lab Software
Technology
Seminar47

Machine Learning for CEGIS• Adapt ML models and algorithms to implement Learner• Piecewise linear classifiers [Sharma+ ’13a, Garg+ ’14, Unno+ ’20]
• Decision trees [Krishna+ ’15, Garg+ ’16, Champion+ ’18, Ezudheen+ ’18, Zhu+ ’18]
• Neural networks [Chang+ ’19, Zhao+ ’20, Abate+ ’21]
• Greedy set covering w/ logic minimization [Padhi+ ’16, Sharma+ ’13b]• Metropolis Hastings MCMC sampler [Sharma+ ’14]
• Probabilistic inference, survey propagation [Satake+ ’20]
• Ensemble learning [Padhi+ ’20]

• Learning to learn• Reinforcement learning of NNs to generate candidates [Si ’18]
• Reinforcement learning of strategy to adjust classification models usedby Learner (joint work w/ Tsukada, Sekiyama, Suenaga)
2020/12/18

STAIR Lab Software Technology Seminar48

SMT-based Piecewise Linear Classification(aka Template-based Synthesis)
1. Prepare a solution template with unknown coefficients,
2. Generate constraints on them, and3. Solve them using an SMT solver
Examples: 𝓔𝓔 ≡ 𝐼𝐼 0 , 𝐼𝐼 0 ⇒ 𝐼𝐼 1 , ¬𝐼𝐼 −1

Solution Template: 𝐼𝐼 𝑥𝑥 ↦ 𝑐𝑐1 ⋅ 𝑥𝑥 + 𝑐𝑐2 ≥ 0

Coeff. Constraints: 𝑐𝑐2 ≥ 0, 𝑐𝑐2 ≥ 0 ⇒ 𝑐𝑐1 + 𝑐𝑐2 ≥ 0, −𝑐𝑐1 + 𝑐𝑐2 < 0Satisfying Assignment: 𝑐𝑐1 ↦ 1, 𝑐𝑐2 ↦ 0

2020/12/18

A Candidate Solution: 𝜌𝜌 ≡ 𝐼𝐼 𝑥𝑥 ↦ 𝑥𝑥 ≥ 0
STAIR Lab Software Technology Seminar

49

Decision Tree Learning
1. Consistently label atoms in 𝓔𝓔 with +/− using a SAT solver
2. Generate a set 𝑄𝑄 of predicates used in classification

3. Classify atoms in 𝓔𝓔 with 𝑄𝑄 using a decision tree learner
Examples: 𝓔𝓔 ≡ 𝐼𝐼 0 , 𝐼𝐼 0 ⇒ 𝐼𝐼 1 , ¬𝐼𝐼 −1

Labeling: 𝐼𝐼 0 ↦ +, 𝐼𝐼 1 ↦ +, 𝐼𝐼 −1 ↦ −𝑥𝑥 ≥ 0, 𝑥𝑥 ≤ 0, 𝑥𝑥 ≥ 1,
Predicates: 𝑄𝑄 ≡𝑥𝑥 ≥ −1, 𝑥𝑥 ≤ 1, 𝑥𝑥 ≤ −1
2020/12/18

Classifier: 𝜌𝜌 ≡ 𝐼𝐼 𝑥𝑥 ↦ 𝑥𝑥 ≥ 0

STAIR Lab Software Technology Seminar

50Template-based Synthesis
vs Decision Tree Learning• Template-based Synthesis (TB)

•  Fixes the shape of solution (updated upon failure)•  Flexibly find necessary predicates via SMT solving•  Atoms in 𝓔𝓔 are consistently labeled using 𝓔𝓔 as an SMT formula• Decision Tree Learning (DT)•  Fixes the predicates of solution (updated upon failure)•  Flexibly adjust the shape based on information gain
•  Atoms are consistently labeled using 𝓔𝓔 as a SAT formula• Evaluation on SyGuS-Comp’19 Inv track XC benchmarks• TB solved 228 instances (out of 276) and DT solved 180 instances
2020/12/18

STAIR Lab Software Technology Seminar

51

Future Research Directions• Efficient synthesis of complex and large functions
from complex and large constraints• (Co)Inductive functions• Functions over (linked, (co)algebraic, array) data structures• Improve labeling, sampling and filtering of examples, andgeneration and ranking of predicates• Convergence theory of CEGIS• More applications

2020/12/18

STAIR Lab Software Technology Seminar

52

Summary• Various program verification and synthesis problems
can be reduced to constraint solving problems• The separation of constraint generation and solving
facilitate tool development• CEGIS-based constraint solving integrates deductive
and inductive reasoning to address challenges• Deductive reasoning by theorem proving (e.g., SAT, SMT)
• Inductive reasoning by machine learning (e.g., decision
tree learning, reinforcement learning)
2020/12/18

STAIR Lab Software Technology Seminar

53