A Fixpoint Logic andDependent Effects for
Temporal Property Verification
Yoji Nanjo1, Hiroshi Unno1, Eric Koskinen2, Tachio Terauchi3
1 University of Tsukuba 2 Stevens Institute of Technology 3 Waseda University

2018/7/11

LICS'18, Oxford, UK1

Temporal Property Verification
Program?

Temporal property

𝑃𝑃 ⊨ Φ
Check whether 𝑃𝑃 satisfies Φ

2018/7/11

LICS'18, Oxford, UK2

This Work
Higher-orderfunctional program?

Value-dependent
temporal property

𝑃𝑃 ⊨ Φ

Check whether 𝑃𝑃 satisfies Φ by using(1) a dependent refinement type & effect system and(2) a deductive system for a first-order fixpoint logic
2018/7/11

LICS'18, Oxford, UK3

Main Contribution• Foundation for compositional & algorithmic
verification of value-dependent temporal
properties of higher-order programs• cf. previous proposals are:• fully automated but whole program analysis[Kobayashi+ PLDI’11], [U.+ POPL’13], [Kuwahara+ESOP’14], [Kuwahara+ CAV’15], [Murase+ POPL’16]• compositional but no support of the class of properties[Koskinen+ CSL-LICS’14], [U.+ POPL’18]

2018/7/11

LICS'18, Oxford, UK4

This WorkHigher-orderfunctional program?

Value-dependent
temporal property𝑃𝑃 ⊨ Φ

Check whether 𝑃𝑃 satisfies Φ by using(1) a dependent refinement type & effect system and(2) a deductive system for a first-order fixpoint logic
2018/7/11

LICS'18, Oxford, UK

5

Example: Functional Program
let rec send_msgs n =emit Send event
if n = 0 then ()else (event[Send]; send_msgs (n-1))

2018/7/11

Generated event sequences:
n < 0 ∶ Send𝜔𝜔 (infinite repetition of Send)
n = 0 ∶ 𝜖𝜖(empty sequence)n = 1 ∶ Sendn = 2 ∶ Send, Send⋮
LICS'18, Oxford, UK

6

This Work
Higher-orderfunctional program?

Value-dependent
temporal property

𝑃𝑃 ⊨ Φ

Check whether 𝑃𝑃 satisfies Φ by using(1) a dependent refinement type & effect system and(2) a deductive system for a first-order fixpoint logic
2018/7/11

LICS'18, Oxford, UK

7

This Work?

predicate for finite
event sequencespredicate for infinite
event sequences

𝑃𝑃 ⊨ Φ𝜇𝜇 , Φ𝜈𝜈

Check whether finite event sequences generated
by 𝑃𝑃 satisfy Φ𝜇𝜇 and infinite event sequences
generated by 𝑃𝑃 satisfy Φ𝜈𝜈2018/7/11LICS'18, Oxford, UK8

Example: Value-Dependent
Temporal Property
let rec send_msgs n =if n = 0 then()else(event[Send];send_msgs (n-1))
n < 0 ∶ Send𝜔𝜔n = 0 ∶ 𝜖𝜖n = 1 ∶ Sendn = 2 ∶ Send, Send⋮
2018/7/11

For terminating
executions⊨Φ𝜇𝜇 ≡ 𝜆𝜆𝜆𝜆 ∈ Σ ∗ . 𝑥𝑥 = SendnΦ𝜈𝜈 ≡ 𝜆𝜆𝜆𝜆 ∈ Σ 𝜔𝜔 . 𝑥𝑥 = Send𝜔𝜔For diverging
executions

LICS'18, Oxford, UKn-times
repetition of Send

infinite repetitionof Send
9

Further Examples• See the paper for further examples that
demonstrate the range of applications

2018/7/11

LICS'18, Oxford, UK10

This Work
Higher-orderfunctional program?

Value-dependent
temporal property

𝑃𝑃 ⊨ Φ

Check whether 𝑃𝑃 satisfies Φ via(1) a dependent refinement type & effect system and(2) a deductive system for a first-order fixpoint logic
2018/7/11

LICS'18, Oxford, UK11

Contributions
1. A dependent refinement type & effect system forcompositional & algorithmic temporal verification• Compositional analysis of dependent temporal effects
represented by predicates of first-order fixpoint logic 𝓛𝓛• Algorithmic type checking via validity checking for ℒ

2. A deductive system for the validity of ℒ

• Use invariants and well-founded relations toover- and under-approximate fixpoints• Designed by transferring ideas from verification research• Can be used with any background first-order theory• Enable other applications to program verification,
which will be presented at the HCVS workshop on 13th

2018/7/11

LICS'18, Oxford, UK12

Contributions
1. A dependent refinement type & effect system forcompositional & algorithmic temporal verification• Compositional analysis of dependent temporal effects
represented by predicates of first-order fixpoint logic 𝓛𝓛• Algorithmic type checking via validity checking for ℒ

2. A deductive system for the validity of ℒ

• Use invariants and well-founded relations toover- and under-approximate fixpoints• Designed by transferring ideas from verification research• Can be used with any background first-order theory• Enable other applications to program verification,
which will be presented at the HCVS workshop on 13th

2018/7/11

LICS'18, Oxford, UK13

First-Order Fixpoint Logic ℒ• First-order logic extended with least fixpoints(LFPs) and greatest fixpoints (GFPs)
predicatevariables

function symbols of
the background theory

predicate symbols of
the background theory

LFPs (𝑋𝑋 occurs
only positively in 𝜙𝜙)

the set of finite
event sequences

GFPs (𝑋𝑋 occurs
only positively in 𝜙𝜙)

the set of infinite
event sequences

We here fix the theory as the one above for temporal effect analysis ,though we could choose any background first-order theory

2018/7/11

LICS'18, Oxford, UK14

Temporal Effect Analysis
functional program𝜇𝜇(Φ𝑒𝑒 , Φ𝑒𝑒𝜈𝜈 )𝑒𝑒

Example:let rec send_msgs n =if n = 0 then ()else (event[Send]; send_msgs (n-1))
predicate variable that relates 𝑛𝑛
and the finite event sequence 𝑥𝑥

𝜇𝜇Φ𝑒𝑒 ≡ 𝜆𝜆𝜆𝜆 ∈ Σ ∗ . (𝜇𝜇𝑋𝑋𝜇𝜇 𝑛𝑛, 𝑥𝑥 .

dependent temporal
effect that describe thetemporal behavior of 𝑒𝑒

The use of first-order fixpoint logic
allows precise representation(cf. previous work only allowed(𝜔𝜔-)regular expressions [Skalka+’08,Hofmann+’14] or did not specify theeffect language [Koskinen+’14])

𝑛𝑛 = 0 ∧ 𝑥𝑥 = 𝜖𝜖 ∨𝑛𝑛 ≠ 0 ∧ ∃𝑦𝑦. 𝑥𝑥 = 𝐒𝐒𝐒𝐒𝐒𝐒𝐒𝐒 ⋅ 𝑦𝑦 ∧ 𝑋𝑋𝜇𝜇 𝑛𝑛 − 1, 𝑦𝑦)(𝑛𝑛, 𝑥𝑥)Φ𝑒𝑒𝜈𝜈 ≡ 𝜆𝜆𝜆𝜆 ∈ Σ 𝜔𝜔 . (𝜈𝜈𝑋𝑋𝜈𝜈 𝑛𝑛, 𝑥𝑥 . 𝑛𝑛 ≠ 0 ∧ ∃𝑦𝑦. 𝑥𝑥 = 𝐒𝐒𝐒𝐒𝐒𝐒𝐒𝐒 ⋅ 𝑦𝑦 ∧ 𝑋𝑋𝜈𝜈 𝑛𝑛 − 1, 𝑦𝑦 )(𝑛𝑛, 𝑥𝑥)predicate variable that relates 𝑛𝑛
and2018/7/11
the infinite event sequence 𝑥𝑥LICS'18, Oxford, UK15

Dependent Refinement Type & Effect System
Type EnvironmentΓ ⊢ 𝑒𝑒 ∶ (𝜏𝜏 & (Φ𝜇𝜇 , Φ𝜈𝜈 ))Program

Dependent Refinement TypeDependent
Temporal Effect

Extends existing refinement type systems [Koskinen+’14, Rondon+’08, U.+’09, Terauchi’10, …]• Types & effects facilitate compositional analysis of dependent temporal effects• Fixpoint logic deduction ⊩ enables algorithmic type checking

Key typing rules:

Sequential composition of effects

Fixpoints describing a dependent
temporal effect of a recursive function
Subtyping

Check sub-effectrelation via fixpoint
logic deduction

Theorem 1 (Soundness): Γ ⊢ 𝑒𝑒 ∶ 𝜏𝜏 & Φ𝜇𝜇 , Φ𝜈𝜈 implies 𝑒𝑒 ∈ Γ ⊢ 𝜏𝜏 & Φ𝜇𝜇 , Φ𝜈𝜈𝜇𝜇 , Φ𝜈𝜈(𝑒𝑒 behaves
undera valuation conforming16to Γ)
2018/7/11 as specified by 𝜏𝜏& Φ
LICS'18,Oxford,
UK

Contributions
1. A dependent refinement type & effect system forcompositional & algorithmic temporal verification• Compositional analysis of dependent temporal effects
represented by predicates of first-order fixpoint logic 𝓛𝓛• Algorithmic type checking via validity checking for ℒ

2. A deductive system for the validity of ℒ

• Use invariants and well-founded relations toover- and under-approximate fixpoints• Designed by transferring ideas from verification research• Can be used with any background first-order theory• Enable other applications to program verification,
which will be presented at the HCVS workshop on 13th

2018/7/11

LICS'18, Oxford, UK17

First-Order Fixpoint Logic ℒ(revisited)• First-order logic extended with least fixpoints(LFPs) and greatest fixpoints (GFPs)
predicatevariables

predicate symbols ofthe background theory

function symbols ofthe background theory
2018/7/11

LFPs(𝑋𝑋 occurs only
positively in 𝜙𝜙)
LICS'18, Oxford, UKsorts (e.g. ℤ) of thebackground theory

GFPs(𝑋𝑋 occurs onlypositively in 𝜙𝜙)18

Deductive System ⊩ 𝜙𝜙 for
the Validity of ℒ

1. Over- and under-approximate fixpoint subformulasof 𝜙𝜙 by non-fixpoint formulas• For soundness, subformulas that occur positively andnegatively are respectively under- and over-approximated

2. Resulting non-fixpoint formulas are discharged bya solver for the background first-order theory• Techniques for obtaining approximations:Over-Approximation

Under-Approximation

LFP

Invariant (induction)

Well-founded relation

GFP

Well-founded relation

Invariant (co-induction)

Analogous to techniques in safety and liveness property verification
2018/7/11

LICS'18, Oxford, UK19

Example: Fixpoint Deduction via
Over-Approx. of LFPCheck that 𝑝𝑝 is a pre-fixpoint of 𝐹𝐹(or, equivalently, perform induction
by unfolding LFP and applying I.H.
to the recursive occurrences of 𝑋𝑋)

Deduction in background first-order theory⊨ 𝑝𝑝 𝑥𝑥 ⇒ 𝑥𝑥 = Send𝑛𝑛⊨ 𝐹𝐹 𝑝𝑝 𝑥𝑥 ⇒ 𝑝𝑝 𝑥𝑥⊩ 𝑝𝑝 𝑥𝑥 ⇒ 𝑥𝑥 = Send𝑛𝑛𝜇𝜇⊩ Φ𝑒𝑒 𝑥𝑥 ⇒ 𝑥𝑥 = Send𝑛𝑛
Over-approx. of LFP
𝜆𝜆𝜆𝜆 ∈ Σ ∗ . 𝑥𝑥 = Send𝑛𝑛
by pre-fixpoint𝜆𝜆𝜆𝜆 ∈ Σ ∗ . 𝜇𝜇𝑋𝑋𝜇𝜇 𝑛𝑛, 𝑥𝑥 . 𝐹𝐹 𝑋𝑋𝜇𝜇 𝑛𝑛, 𝑥𝑥

where 𝐹𝐹 𝑋𝑋 𝑛𝑛, 𝑥𝑥 =2018/7/11

𝑛𝑛, 𝑥𝑥𝑛𝑛 = 0 ∧ 𝑥𝑥 = 𝜖𝜖 ∨𝑛𝑛 ≠ 0 ∧ ∃𝑦𝑦. 𝑥𝑥 = Send ⋅ 𝑦𝑦 ∧ 𝑋𝑋 𝑛𝑛 − 1, 𝑦𝑦

LICS'18, Oxford, UK20

Example: Fixpoint Deduction via
Over-Approx. of GFPCheck that the given well-founded relation 𝑝𝑝2
witnesses that the given predicate 𝒑𝒑𝟏𝟏 and 𝚽𝚽𝒆𝒆𝝂𝝂have no intersection (see the paper for details)

Deduction in backgroundfirst-order theory

𝑝𝑝1 𝑛𝑛, 𝑥𝑥 ∧ 𝑛𝑛 ≠ 0 ∧ 𝑥𝑥 = Send ⋅ 𝑥𝑥 ′ ⇒⊨𝑝𝑝1 (𝑛𝑛 − 1, 𝑥𝑥 ′ ∧ 𝑝𝑝2 (𝑛𝑛, 𝑥𝑥, 𝑛𝑛 − 1, 𝑥𝑥𝑥))⋮𝑋𝑋𝜈𝜈 𝑛𝑛, 𝑥𝑥 ; 𝑝𝑝1 ; 𝑝𝑝2 ; ⊤ ↑� 𝑛𝑛 ≠ 0 ∧ ∃𝑦𝑦. 𝑥𝑥 = Send ⋅ 𝑦𝑦 ∧ 𝑋𝑋𝜈𝜈 (𝑛𝑛 − 1, 𝑦𝑦)⊩ Φ𝑒𝑒𝜈𝜈 𝑥𝑥 ⇒ 𝑥𝑥 = Send𝜔𝜔𝜆𝜆𝜆𝜆 ∈ Σ𝜔𝜔 . 𝑛𝑛 ≥ 0 ∨ 𝑥𝑥 ≠ Send𝜔𝜔

𝜆𝜆 𝑛𝑛1 , 𝑥𝑥1 , 𝑛𝑛2 , 𝑥𝑥2 . 𝑛𝑛1 > 𝑛𝑛2 ≥ 0
2018/7/11

𝜆𝜆𝜆𝜆 ∈ Σ𝜔𝜔 .

𝜈𝜈𝑋𝑋𝜈𝜈 𝑛𝑛, 𝑥𝑥 . 𝑛𝑛 ≠ 0 ∧LICS'18, Oxford, UK⊨ ¬𝑝𝑝1 𝑥𝑥 ⇒ 𝑥𝑥 = Send𝜔𝜔⊩ ¬𝑝𝑝1 𝑥𝑥 ⇒ 𝑥𝑥 = Send𝜔𝜔Over-approx. of GFPby negation of 𝑝𝑝1∃𝑦𝑦. 𝑥𝑥 = Send ⋅ 𝑦𝑦 ∧𝑋𝑋𝜈𝜈 𝑛𝑛 − 1, 𝑦𝑦

𝑛𝑛, 𝑥𝑥21

Deductive System ⊩ 𝜙𝜙 for ℒ

Over-approximationof LFP (induction)

Backgroundfirst-ordertheory solver

Approximation of fixpoints
using well-founded relation(see the paper for details)

Under-approximationof GFP (co-induction)𝜓𝜓 represents a fixpoint-free formula.

𝑛𝑛𝑛𝑛𝑛𝑛(𝜓𝜓) is negation normal form of 𝜓𝜓.
𝐶𝐶 + (resp. 𝐶𝐶 − ) is positive (resp. negative) context.

Theorem 2 (Soundness of ⊩): ⊩ 𝜙𝜙 implies ⊨ 𝜙𝜙2018/7/11

LICS'18, Oxford, UK22

Conclusion• Foundation for compositional & algorithmic
verification of value-dependent temporal propertiesof higher-order programs
1. Dependent refinement type & effect system• Compositional analysis of dependent temporal effects
represented by predicates of first-order fixpoint logic 𝓛𝓛• Algorithmic type checking via validity checking for ℒ

2. Deductive system for the validity of ℒ
Over-Approximation

Under-Approximation

LFP

Invariant (induction)

Well-founded relation

GFP

Well-founded relation

Invariant (co-induction)• Can be used with any background first-order theory• Enable other applications to program verification,
which will be presented at the HCVS workshop on 13th

2018/7/11

LICS'18, Oxford, UK23