Probabilistic Inference forPredicate Constraint Satisfaction
Hiroshi Unno (University of Tsukuba)
Joint Work with Yuki Satake and Hinata Yanagi

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

Constraints 𝓒𝓒 on Predicate Variables
Constraint
Solving

February 9, 2020

𝓒𝓒 is Sat (𝑷𝑷 satisfies 𝝍𝝍),𝓒𝓒 is Unsat (𝑷𝑷 violates 𝝍𝝍),or Unknown
AAAI'20, NY, USA2

Previous Work: Program Verification via
Constrained Horn Clauses (CHCs) [Bjørner+ ’15]
Target Program 𝑷𝑷 & Specification 𝝍𝝍Limited to Linear-Time
Safety Verification ConstraintGeneration

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

CHCs Constraints 𝓒𝓒 on Predicate Variables

Verification Intermediary
Independent of Particular
Target and Method February 9, 2020

ConstraintSolving

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

𝓒𝓒 is Sat (𝑷𝑷 satisfies 𝝍𝝍),𝓒𝓒 is Unsat (𝑷𝑷 violates 𝝍𝝍),or Unknown
AAAI'20, NY, USA

3

This Work: Program Verification via Predicate
Constraint Satisfaction Problem (pCSP)
Target Program 𝑷𝑷 & Specification 𝝍𝝍Support Branching-Time
Safety Verification Constraint
Generation

New method for Looping& Recursive Programs

pCSP Constraints 𝓒𝓒 on Predicate Variables

Verification Intermediary
Independent of Particular
Target and Method February 9, 2020

ConstraintSolving

New method based on
Probabilistic Inference

𝓒𝓒 is Sat (𝑷𝑷 satisfies 𝝍𝝍),𝓒𝓒 is Unsat (𝑷𝑷 violates 𝝍𝝍),or Unknown
AAAI'20, NY, USA

4

This Work: Program Verification via Predicate
Constraint Satisfaction Problem (pCSP)
Target Program 𝑷𝑷 & Specification 𝝍𝝍Constraint
Generation

pCSP Constraints 𝓒𝓒 on Predicate Variables

Verification Intermediary
Independent of Particular
Target and Method February 9, 2020

ConstraintSolving

𝓒𝓒 is Sat (𝑷𝑷 satisfies 𝝍𝝍),𝓒𝓒 is Unsat (𝑷𝑷 violates 𝝍𝝍),or Unknown
AAAI'20, NY, USA

5

Predicate Constraint
Satisfaction Problem (pCSP)• A finite set 𝓒𝓒 of clauses of the form:

𝑋𝑋1 𝑡𝑡�1 ∨ ⋯ ∨ 𝑋𝑋ℓ 𝑡𝑡�ℓ ∨ 𝜙𝜙 ∨� ∨ ⋯ ∨ ¬𝑋𝑋𝑚𝑚 𝑡𝑡�
¬𝑋𝑋ℓ+1 𝑡𝑡ℓ+1
𝑚𝑚

where 𝑋𝑋1 , … , 𝑋𝑋𝑚𝑚 are predicate variables,𝑡𝑡�1 , … , 𝑡𝑡�
𝑚𝑚 are sequences of terms,
𝜙𝜙 is a first-order formula w/o predicate variables.

February 9, 2020

AAAI'20, NY, USA6

Predicate Constraint
Satisfaction Problem (pCSP)• A finite set 𝓒𝓒 of clauses of the form:

𝑋𝑋1 𝑡𝑡�1 ∨ ⋯ ∨ 𝑋𝑋ℓ 𝑡𝑡�ℓ ⟸� ∧ ⋯ ∧ 𝑋𝑋𝑚𝑚 𝑡𝑡�
𝑋𝑋ℓ+1 𝑡𝑡ℓ+1𝑚𝑚 ∧ ¬𝜙𝜙where 𝑋𝑋1 , … , 𝑋𝑋𝑚𝑚 are predicate variables,𝑡𝑡�1 , … , 𝑡𝑡�
𝑚𝑚 are sequences of terms,
𝜙𝜙 is a first-order formula w/o predicate variables.

• 𝓒𝓒 is satisfiable (modulo first-order theories) if there is aninterpretation 𝜌𝜌 of predicate variables such that 𝜌𝜌 ⊨ ⋀𝓒𝓒• 𝓒𝓒 is called CHCs [Bjørner+ ’15] if ℓ ≤ 1 for each clause in 𝓒𝓒February 9, 2020

AAAI'20, NY, USA

7

This Work: Program Verification via Predicate
Constraint Satisfaction Problem (pCSP)
Target Program 𝑷𝑷 & Specification 𝝍𝝍Support Branching-Time
Safety Verification Constraint
Generation

pCSP Constraints 𝓒𝓒 on Predicate Variables
Constraint
Solving

February 9, 2020

𝓒𝓒 is Sat (𝑷𝑷 satisfies 𝝍𝝍),𝓒𝓒 is Unsat (𝑷𝑷 violates 𝝍𝝍),or Unknown
AAAI'20, NY, USA

8

Branching-Time Safety Verification ofFinitely-Branching Programs• Safety is a class of properties of the form
“something bad will never happen”• Branching-time verification concerns properties ofthe computation tree of the given program that may
exhibit non-deterministic behavior (cf. linear-timeverification concerns properties of execution traces)• Subsumes non-termination verification of deciding
whether there is a non-terminating execution
February 9, 2020

AAAI'20, NY, USA9

This Work: Program Verification via Predicate
Constraint Satisfaction Problem (pCSP)
Target Program 𝑷𝑷 & Specification 𝝍𝝍Constraint
Generation

New method for Looping& Recursive Programs

pCSP Constraints 𝓒𝓒 on Predicate Variables
Constraint
Solving

February 9, 2020

𝓒𝓒 is Sat (𝑷𝑷 satisfies 𝝍𝝍),𝓒𝓒 is Unsat (𝑷𝑷 violates 𝝍𝝍),or Unknown
AAAI'20, NY, USA

10

Prog. & Spec.

pCSP

Constraint Generation

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

∃ 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭

SAT or UNSAT
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
AAAI'20, NY, USA11

Prog. & Spec.

pCSP

Constraint Generation

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

∃ 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭

SAT or UNSAT
Constraint Solving

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

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

AAAI'20, NY, USA

12

Prog. & Spec.

pCSP

Constraint Generation

Input:
𝑥𝑥 > 0𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝑥𝑥 ≠ 0 𝐝𝐝𝐝𝐝𝐢𝐢𝐢𝐢 𝐫𝐫𝐫𝐫𝐫𝐫𝐫𝐫_𝐛𝐛𝐛𝐛𝐛𝐛𝐛𝐛
𝑥𝑥 ← 𝑥𝑥 − 1𝐞𝐞𝐞𝐞𝐞𝐞𝐞𝐞𝑥𝑥 ← 𝑥𝑥 + 1
𝐝𝐝𝐝𝐝𝐝𝐝𝐝𝐝⊥
February 9, 2020

SAT or UNSAT
Constraint Solving

represents a loop invariant
Output 𝓒𝓒: preserved by some execution① 𝐼𝐼 𝑥𝑥 ⟸ 𝑥𝑥 > 0,
∃ 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭② 𝐼𝐼 𝑥𝑥 − 1 ∨ 𝐼𝐼 𝑥𝑥 + 1
𝓒𝓒 is beyond⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 ≠ 0,CHCs!
③ ⊥ ⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 = 0
𝓒𝓒 is satisfiable, witnessed bya NY,solution
𝐼𝐼 𝑥𝑥 ≡ 𝑥𝑥 > 0 13
AAAI'20,USA

This Work: Program Verification via Predicate
Constraint Satisfaction Problem (pCSP)
Target Program 𝑷𝑷 & Specification 𝝍𝝍Constraint
Generation

pCSP Constraints 𝓒𝓒 on Predicate Variables
Constraint
Solving

February 9, 2020

New method based on
Probabilistic Inference

𝓒𝓒 is Sat (𝑷𝑷 satisfies 𝝍𝝍),𝓒𝓒 is Unsat (𝑷𝑷 violates 𝝍𝝍),or Unknown
AAAI'20, NY, USA14

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

We address these challenges by a novel
combination of probabilistic inference withCounterExample Guided Inductive Synthesis(CEGIS) [Solar-Lezama+ ’06]
February 9, 2020

AAAI'20, NY, USA15

CounterExample Guided
Inductive Synthesis (CEGIS)• Iteratively accumulate example instances 𝓔𝓔 of thegiven 𝓒𝓒 through the two phases for each iteration:• Synthesis Phase• Enumerate candidate solutions 𝜌𝜌1 , … , 𝜌𝜌𝑛𝑛 that satisfy 𝓔𝓔• Validation Phase• Check if there is a candidate 𝜌𝜌𝑖𝑖 that also satisfies 𝓒𝓒• If yes, return 𝜌𝜌𝑖𝑖 as a solution of 𝓒𝓒• If no, repeat the procedure with new example instances
witnessing non-satisfaction of 𝓒𝓒 by 𝜌𝜌1 , … , 𝜌𝜌𝑛𝑛 added

February 9, 2020

AAAI'20, NY, USA

16

Example Run of CEGIS
Synthesizer

Validator

Example Instances 𝓔𝓔:

pCSP Constraints 𝓒𝓒:∅Starting fromthe empty set• 𝐼𝐼 𝑥𝑥 ⟸ 𝑥𝑥 > 0• 𝐼𝐼 𝑥𝑥 − 1 ∨ 𝐼𝐼 𝑥𝑥 + 1⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 ≠ 0• ⊥ ⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 = 0

Is one of the following candidates genuine?
𝐼𝐼 𝑥𝑥 ↦ ⊤ , …

February 9, 2020

AAAI'20, NY, USA

17

Example Run of CEGIS
Synthesizer

Validator

Example Instances 𝓔𝓔:

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

February 9, 2020

No. 𝐼𝐼 𝑥𝑥 ↦ ⊤ is not.
The 3rd clause is violated when 𝑥𝑥 = 0
AAAI'20, NY, USA

18

Example Run of CEGIS
Synthesizer

Validator

Example Instances 𝓔𝓔:

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

Is one of the following candidates genuine?
𝐼𝐼 𝑥𝑥 ↦ 𝑥𝑥 < 0 , …

February 9, 2020

AAAI'20, NY, USA

19

Example Run of CEGIS
SynthesizerValidator

Example Instances 𝓔𝓔:

pCSP Constraints 𝓒𝓒:¬𝐼𝐼 0

𝐼𝐼 1 ⟸ 1 > 0

February 9, 2020

• 𝐼𝐼 𝑥𝑥 ⟸ 𝑥𝑥 > 0• 𝐼𝐼 𝑥𝑥 − 1 ∨ 𝐼𝐼 𝑥𝑥 + 1⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 ≠ 0• ⊥ ⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 = 0No. 𝐼𝐼 𝑥𝑥 ↦ 𝑥𝑥 < 0 is not.
The 1st clause is violated when 𝑥𝑥 = 1
AAAI'20, NY, USA20

Example Run of CEGIS
Synthesizer

Validator

Example Instances 𝓔𝓔:

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

Is one of the following candidates genuine?
𝐼𝐼 𝑥𝑥 ↦ 𝑥𝑥 ≥ 1 , …

February 9, 2020

AAAI'20, NY, USA

21

Example Run of CEGIS
SynthesizerValidator

Example Instances 𝓔𝓔:

pCSP Constraints 𝓒𝓒:¬𝐼𝐼 0
𝐼𝐼 1February 9, 2020

• 𝐼𝐼 𝑥𝑥 ⟸ 𝑥𝑥 > 0• 𝐼𝐼 𝑥𝑥 − 1 ∨ 𝐼𝐼 𝑥𝑥 + 1⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 ≠ 0• ⊥ ⟸ 𝐼𝐼 𝑥𝑥 ∧ 𝑥𝑥 = 0

Yes. 𝐼𝐼 𝑥𝑥 ↦ 𝑥𝑥 ≥ 1 is a solution of 𝓒𝓒!
AAAI'20, NY, USA

22

Enumeration of Candidates 𝜌𝜌1 , … , 𝜌𝜌𝑛𝑛• Challenges:

1. The number 𝑛𝑛 of candidates must be bounded
2. Candidates must satisfy 𝓔𝓔 and should be simpler(per Occam’s razor) and essentially different each otherfor more chance to satisfy 𝓒𝓒• Our Solutions:

1. Compute predicate abstraction [Graf+ ’97] 𝛼𝛼 𝓔𝓔 of 𝓔𝓔 using
a finite set 𝓠𝓠 of predicates to reduce the search space ofcandidates to the finite set of 𝓠𝓠-expressible solutions
2. Enumerate “promising” satisfying Boolean assignmentsof 𝛼𝛼 𝓔𝓔 via survey inspired decimation (SID) [Braunstein+ ’05]
February 9, 2020

AAAI'20, NY, USA

23

Example: Predicate Abstraction
Example Instances 𝓔𝓔:• ¬𝐼𝐼 0• 𝐼𝐼 1

February 9, 2020

Predicates Set 𝓠𝓠:
𝜆𝜆𝜆𝜆. ⊥, 𝜆𝜆𝜆𝜆. ⊤,𝜆𝜆𝜆𝜆. 𝑥𝑥 ≥ 0, 𝜆𝜆𝜆𝜆. −𝑥𝑥 ≥ 0,𝜆𝜆𝜆𝜆. 𝑥𝑥 ≥ 1, 𝜆𝜆𝜆𝜆. −𝑥𝑥 ≥ −1

AAAI'20, NY, USA

24

Example: Predicate Abstraction
Example Instances 𝓔𝓔:• ¬𝐼𝐼 0• 𝐼𝐼 1

Predicates Set 𝓠𝓠:
𝜆𝜆𝜆𝜆. ⊥, 𝜆𝜆𝜆𝜆. ⊤,𝜆𝜆𝜆𝜆. 𝑥𝑥 ≥ 0, 𝜆𝜆𝜆𝜆. 0 ≥ 𝑥𝑥,𝜆𝜆𝜆𝜆. 𝑥𝑥 ≥ 1, 𝜆𝜆𝜆𝜆. 1 ≥ 𝑥𝑥

Solution Template with Boolean parameters 𝑏𝑏⊥ , 𝑏𝑏≥1 , 𝑏𝑏0≥ ,…:𝐼𝐼 𝑥𝑥 ↦ 𝑏𝑏⊥ ⇒⊥ ∧ 𝑏𝑏≥1 ⇒ 𝑥𝑥 ≥ 1 ∧ 𝑏𝑏0≥ ⇒ 0 ≥ 𝑥𝑥 ∧ ⋯Predicate Abstraction 𝛼𝛼 𝓔𝓔 ≡ 𝑏𝑏⊥ ∨ 𝑏𝑏≥1 ∧ ¬𝑏𝑏⊥ ∧ ¬𝑏𝑏0≥
Satisfying Assignments for 𝛼𝛼 𝓔𝓔 : don’t care𝑏𝑏⊥ ↦⊥, 𝑏𝑏0≥ ↦⊥, 𝑏𝑏≥1 ↦ ⊤, 𝑏𝑏⊤ ↦∗, 𝑏𝑏≥0 ↦∗, 𝑏𝑏1≥ ↦∗ , indicating that
𝝀𝝀𝝀𝝀. ⊥ and 𝝀𝝀𝝀𝝀. 𝟎𝟎 ≥ 𝒙𝒙 must not be used and 𝝀𝝀𝝀𝝀. 𝒙𝒙 ≥ 𝟏𝟏 must be used
∴ 𝓠𝓠-expressible
sols. are 𝐼𝐼 𝑥𝑥 AAAI'20,↦ 𝑥𝑥 NY,≥USA1 and 𝐼𝐼 𝑥𝑥 ↦ 𝑥𝑥 ≥ 1 ∧ 1 25≥ 𝑥𝑥
February 9, 2020

SID-based Enumeration of “Promising ”
Satisfying Assignments for 𝛼𝛼 𝓔𝓔• To obtain a simpler solution (e.g., 𝐼𝐼 𝑥𝑥 ↦ 𝑥𝑥 ≥ 1 ),detect and assign ⊥ to the don’t-care variables• To reduce similar solutions while preserving different
ones belonging to different solution clusters, use SID toiteratively assign a value 𝑣𝑣 to a variable of 𝛼𝛼 𝓔𝓔 with thehighest bias toward 𝑣𝑣 (i.e., “sufficiently” determined)• The biases of each variable are computed via probabilistic
inference (survey propagation) in a graphical model (factorgraph) obtained from 𝛼𝛼 𝓔𝓔 (see the paper for details)

February 9, 2020

AAAI'20, NY, USA26

Evaluation• Implemented the presented method as a pCSP solver
PCSat using Z3 as the backend SMT solver• Tested PCSat on the benchmark sets from• SyGuS-Comp 2017 and 2018 (Invariant Synthesis Track)• CHC-COMP 2019 (LIA-nonlin Track)• New pCSP benchmarks of branching-time safety verificationthat go beyond the scope of existing SyGuS and CHC solvers

February 9, 2020

AAAI'20, NY, USA

27

Results on 127 Benchmarks
from SyGuS-Comp 2018

February 9, 2020

AAAI'20, NY, USA28

Summary: Program Verification via Predicate
Constraint Satisfaction Problem (pCSP)
Target Program 𝑷𝑷 & Specification 𝝍𝝍Support Branching-Time
Safety Verification Constraint
Generation

New method for Looping& Recursive Programs

pCSP Constraints 𝓒𝓒 on Predicate Variables

Verification Intermediary
Independent of Particular
Target and Method February 9, 2020

ConstraintSolving

New method based on
CEGIS, Pred. Abstraction,
Survey Inspired Decimation

𝓒𝓒 is Sat (𝑷𝑷 satisfies 𝝍𝝍),𝓒𝓒 is Unsat (𝑷𝑷 violates 𝝍𝝍),or Unknown
AAAI'20, NY, USA29

Ongoing and Future Work
Extend pCSP to support branching-time liveness verification of(possibly) infinitely branching programs• Liveness: “something good will eventually happen”

Develop constraint generation tools for C, Java, OCaml, 𝜇𝜇CLP
Extend PCSat to support more theories (Arrays, ADTs, heaps, …)• Apply other constraint satisfaction methods to enumerate sols.
• Apply other probabilistic inference like variational inference
and approximate model counting by directly modeling pCSP asfactor graphs representing joint probability distributions overrandom predicate variables
February 9, 2020

AAAI'20, NY, USA30