Propositional Dynamic Logic forHigher-Order Functional Programs
Yuki Satake (University of Tsukuba)
Hiroshi Unno (University of Tsukuba)

CAV'18, Oxford, United Kingdom

1

Higher-Order Functional Programs• A higher-order function takes a function as its argument
and/or returns a function as its return value

𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 ∶ 𝐢𝐢𝐢𝐢𝐢𝐢 → 𝐢𝐢𝐢𝐢𝐢𝐢 → 𝐢𝐢𝐢𝐢𝐢𝐢 → 𝐢𝐢𝐢𝐢𝐢𝐢
𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝒇𝒇 𝒙𝒙 = 𝒇𝒇 (𝒇𝒇 𝒙𝒙)• Support in Programming Languages:• OCaml, Haskell, Rust
• Jave(+1.8), Scala, Ruby, Python

CAV'18, Oxford, United Kingdom

Contribute significantly
to modularity2

Higher-Order Functional Programs• A higher-order function takes a function as its argument
and/or returns a function as its return value
takes a function as its argument

𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 ∶ 𝐢𝐢𝐢𝐢𝐢𝐢 → 𝐢𝐢𝐢𝐢𝐢𝐢 → 𝐢𝐢𝐢𝐢𝐢𝐢 → 𝐢𝐢𝐢𝐢𝐢𝐢
𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝒇𝒇 𝒙𝒙 = 𝒇𝒇 (𝒇𝒇 𝒙𝒙)• Support in Programming Languages:• OCaml, Haskell, Rust
• Jave(+1.8), Scala, Ruby, Python

CAV'18, Oxford, United Kingdom

Contribute significantly
to modularity3

Higher-Order Functional Programs• A higher-order function takes a function as its argument
and/or returns a function as its return value
takes a function as its argument

returns a function as its result

𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 ∶ 𝐢𝐢𝐢𝐢𝐢𝐢 → 𝐢𝐢𝐢𝐢𝐢𝐢 → 𝐢𝐢𝐢𝐢𝐢𝐢 → 𝐢𝐢𝐢𝐢𝐢𝐢
𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝒇𝒇 𝒙𝒙 = 𝒇𝒇 (𝒇𝒇 𝒙𝒙)• Support in Programming Languages:• OCaml, Haskell, Rust
• Jave(+1.8), Scala, Ruby, Python

CAV'18, Oxford, United Kingdom

Contribute significantly
to modularity
4

Higher-Order Functional Programs• A higher-order function takes a function as its argument
and/or returns a function as its return value
takes a function as its argument

returns a function as its result

𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 ∶ 𝐢𝐢𝐢𝐢𝐢𝐢 → 𝐢𝐢𝐢𝐢𝐢𝐢 → 𝐢𝐢𝐢𝐢𝐢𝐢 → 𝐢𝐢𝐢𝐢𝐢𝐢
𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝒇𝒇 𝒙𝒙 = 𝒇𝒇 (𝒇𝒇 𝒙𝒙)• Support in Programming Languages:• OCaml, Haskell, Rust
• Jave(+1.8), Scala, Ruby, Python

CAV'18, Oxford, United Kingdom

Contribute significantly
to modularity
5

Example: Higher-Order Program

Reduction Sequence for r=0

Higher Order Program

𝐥𝐥𝐥𝐥𝐥𝐥 𝒓𝒓 = ∗ 𝐢𝐢𝐢𝐢
𝐥𝐥𝐥𝐥𝐥𝐥 𝐢𝐢𝐢𝐢𝐢𝐢 𝒙𝒙 = 𝒙𝒙 + 𝟏𝟏 𝐢𝐢𝐢𝐢
𝐥𝐥𝐥𝐥𝐥𝐥 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝒇𝒇 𝒙𝒙 = 𝒇𝒇 (𝒇𝒇 𝒙𝒙) 𝐢𝐢𝐢𝐢
𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝐢𝐢𝐢𝐢𝐢𝐢 𝒓𝒓
CAV'18, Oxford, United Kingdom

𝐭𝐭𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎

6

Example: Higher-Order Program
Non-deterministic integer
Reduction Sequence for r=0

Higher Order Program

𝐥𝐥𝐥𝐥𝐥𝐥 𝒓𝒓 = ∗ 𝐢𝐢𝐢𝐢
𝐥𝐥𝐥𝐥𝐥𝐥 𝐢𝐢𝐢𝐢𝐢𝐢 𝒙𝒙 = 𝒙𝒙 + 𝟏𝟏 𝐢𝐢𝐢𝐢
𝐥𝐥𝐥𝐥𝐥𝐥 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝒇𝒇 𝒙𝒙 = 𝒇𝒇 (𝒇𝒇 𝒙𝒙) 𝐢𝐢𝐢𝐢
𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝐢𝐢𝐢𝐢𝐢𝐢 𝒓𝒓
CAV'18, Oxford, United Kingdom

𝐭𝐭𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎

6

Example: Higher-Order Program
Non-deterministic integer
Reduction Sequence for r=0

Higher Order Program

𝐥𝐥𝐥𝐥𝐥𝐥 𝒓𝒓 = ∗ 𝐢𝐢𝐢𝐢
𝐥𝐥𝐥𝐥𝐥𝐥 𝐢𝐢𝐢𝐢𝐢𝐢 𝒙𝒙 = 𝒙𝒙 + 𝟏𝟏 𝐢𝐢𝐢𝐢
𝐥𝐥𝐥𝐥𝐥𝐥 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝒇𝒇 𝒙𝒙 = 𝒇𝒇 (𝒇𝒇 𝒙𝒙) 𝐢𝐢𝐢𝐢
𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝐢𝐢𝐢𝐢𝐢𝐢 𝒓𝒓

Higher-Order function 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭

CAV'18, Oxford, United Kingdom

𝐭𝐭𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎

6

Example: Higher-Order Program
Non-deterministic integer
Higher Order Program

Reduction Sequence for r=0

𝐥𝐥𝐥𝐥𝐥𝐥 𝒓𝒓 = ∗ 𝐢𝐢𝐢𝐢
𝐥𝐥𝐥𝐥𝐥𝐥 𝐢𝐢𝐢𝐢𝐢𝐢 𝒙𝒙 = 𝒙𝒙 + 𝟏𝟏 𝐢𝐢𝐢𝐢
𝐥𝐥𝐥𝐥𝐥𝐥 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝒇𝒇 𝒙𝒙 = 𝒇𝒇 (𝒇𝒇 𝒙𝒙) 𝐢𝐢𝐢𝐢
𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝐢𝐢𝐢𝐢𝐢𝐢 𝒓𝒓

𝐭𝐭𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎→ (𝛌𝛌𝛌𝛌. 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝐱𝐱)) 𝟎𝟎

Higher-Order function 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭

CAV'18, Oxford, United Kingdom

6

Example: Higher-Order Program
Non-deterministic integer
Higher Order Program

Reduction Sequence for r=0

𝐥𝐥𝐥𝐥𝐥𝐥 𝒓𝒓 = ∗ 𝐢𝐢𝐢𝐢
𝐥𝐥𝐥𝐥𝐥𝐥 𝐢𝐢𝐢𝐢𝐢𝐢 𝒙𝒙 = 𝒙𝒙 + 𝟏𝟏 𝐢𝐢𝐢𝐢
𝐥𝐥𝐥𝐥𝐥𝐥 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝒇𝒇 𝒙𝒙 = 𝒇𝒇 (𝒇𝒇 𝒙𝒙) 𝐢𝐢𝐢𝐢
𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝐢𝐢𝐢𝐢𝐢𝐢 𝒓𝒓

𝐭𝐭𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎→ (𝛌𝛌𝛌𝛌. 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝐱𝐱)) 𝟎𝟎→ 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎)

Higher-Order function 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭

CAV'18, Oxford, United Kingdom

6

Example: Higher-Order Program
Non-deterministic integer
Higher Order Program

Reduction Sequence for r=0

𝐥𝐥𝐥𝐥𝐥𝐥 𝒓𝒓 = ∗ 𝐢𝐢𝐢𝐢
𝐥𝐥𝐥𝐥𝐥𝐥 𝐢𝐢𝐢𝐢𝐢𝐢 𝒙𝒙 = 𝒙𝒙 + 𝟏𝟏 𝐢𝐢𝐢𝐢
𝐥𝐥𝐥𝐥𝐥𝐥 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝒇𝒇 𝒙𝒙 = 𝒇𝒇 (𝒇𝒇 𝒙𝒙) 𝐢𝐢𝐢𝐢
𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝐢𝐢𝐢𝐢𝐢𝐢 𝒓𝒓

𝐭𝐭𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎→ (𝛌𝛌𝛌𝛌. 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝐱𝐱)) 𝟎𝟎→ 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎)→∗ 𝐢𝐢𝐢𝐢𝐢𝐢 𝟏𝟏 →∗ 𝟐𝟐

Higher-Order function 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭

CAV'18, Oxford, United Kingdom

6Temporal Verification of Higher-Order
Programs• Specification languages used in existing verification methods• (𝝎𝝎-)regular word languages (that subsume LTL) [Disney+ ’11; Hofmann+ ’14; Murase+ ’16]
• Modal 𝝁𝝁-calculus (that subsumes CTL) [Fujima+ ’13; Lester+ ’11; Suzuki+ ’17]
• (Extended) dependent refinement types• Temporal properties [Koskinen+ ’14; Nanjo+ ’18]
• Temporal and branching properties [Unno+ ’18]

CAV'18, Oxford, United Kingdom

7Temporal Verification of Higher-Order
Programs• Specification languages used in existing verification methods• (𝝎𝝎-)regular word languages (that subsume LTL) [Disney+ ’11; Hofmann+ ’14; Murase+ ’16]
• Modal 𝝁𝝁-calculus (that subsumes CTL) [Fujima+ ’13; Lester+ ’11; Suzuki+ ’17]
• (Extended) dependent refinement types• Temporal properties [Koskinen+ ’14; Nanjo+ ’18]
• Temporal and branching properties [Unno+ ’18]

 they cannot sufficiently express temporal specifications
that involve higher-order functions
CAV'18, Oxford, United Kingdom

7

Example: Property that cannot be expressedby the previous specification languages
𝐭𝐭𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎→ (𝛌𝛌𝛌𝛌. 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝐱𝐱)) 𝟎𝟎→ 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎)→∗ 𝐢𝐢𝐢𝐢𝐢𝐢 𝟏𝟏 →∗ 𝟐𝟐

If the function returned by a partial application of twice tosome function is called with some integer n, then the function
argument passed to twice is eventually called with n
CAV'18, Oxford, United Kingdom

8

Example: Property that cannot be expressedby the previous specification languages
𝐭𝐭𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎→ (𝛌𝛌𝛌𝛌. 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝐱𝐱)) 𝟎𝟎→ 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎)→∗ 𝐢𝐢𝐢𝐢𝐢𝐢 𝟏𝟏 →∗ 𝟐𝟐

If the function returned by a partial application of twice tosome function is called with some integer n, then the function
argument passed to twice is eventually called with n
CAV'18, Oxford, United Kingdom

8

Example: Property that cannot be expressedby the previous specification languages
𝐭𝐭𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎→ (𝛌𝛌𝛌𝛌. 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝐱𝐱)) 𝟎𝟎→ 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎)→∗ 𝐢𝐢𝐢𝐢𝐢𝐢 𝟏𝟏 →∗ 𝟐𝟐

If the function returned by a partial application of twice tosome function is called with some integer n, then the function
argument passed to twice is eventually called with n
CAV'18, Oxford, United Kingdom

9

Example: Property that cannot be expressedby the previous specification languages
𝐭𝐭𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎→ (𝛌𝛌𝛌𝛌. 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝐱𝐱)) 𝟎𝟎→ 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎)→∗ 𝐢𝐢𝐢𝐢𝐢𝐢 𝟏𝟏 →∗ 𝟐𝟐

If the function returned by a partial application of twice tosome function is called with some integer n, then the function
argument passed to twice is eventually called with n
CAV'18, Oxford, United Kingdom

10

Example: Property that cannot be expressedby the previous specification languages
𝐭𝐭𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎→ (𝛌𝛌𝛌𝛌. 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝐱𝐱)) 𝟎𝟎→ 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎)→∗ 𝐢𝐢𝐢𝐢𝐢𝐢 𝟏𝟏 →∗ 𝟐𝟐

If the function returned by a partial application of twice tosome function is called with some integer n, then the function
argument passed to twice is eventually called with n
CAV'18, Oxford, United Kingdom

11

Example: Property that cannot be expressedby the previous specification languages
𝐭𝐭𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎→ (𝛌𝛌𝛌𝛌. 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝐱𝐱)) 𝟎𝟎→ 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎)→∗ 𝐢𝐢𝐢𝐢𝐢𝐢 𝟏𝟏 →∗ 𝟐𝟐

If the function returned by a partial application of twice tosome function is called with some integer n, then the function
argument passed to twice is eventually called with n
CAV'18, Oxford, United Kingdom

12

Example: Property that cannot be expressedby the previous specification languages
𝐭𝐭𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎→ (𝛌𝛌𝛌𝛌. 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝐱𝐱)) 𝟎𝟎→ 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎)→∗ 𝐢𝐢𝐢𝐢𝐢𝐢 𝟏𝟏 →∗ 𝟐𝟐

If the function returned by a partial application of twice tosome function is called with some integer n, then the function
argument passed to twice is eventually called with n
CAV'18, Oxford, United Kingdom

13

Example: Property that cannot be expressedby the previous specification languages
𝐭𝐭𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎→ (𝛌𝛌𝛌𝛌. 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝐱𝐱)) 𝟎𝟎→ 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎)→∗ 𝐢𝐢𝐢𝐢𝐢𝐢 𝟏𝟏 →∗ 𝟐𝟐

Previous languages cannot refer tothe control flow of higher-orderprograms involving a function thatis passed to or returned by ahigher-order function

If the function returned by a partial application of twice tosome function is called with some integer n, then the function
argument passed to twice is eventually called with n
CAV'18, Oxford, United Kingdom

14

Our Contributions• Higher-Order Trace (HOT) that captures the control flow ofhigher-order programs• Higher-Order Trace Propositional Dynamic Logic (HOT-PDL):• Propositional Dynamic Logic (PDL) over HOTs for specifying temporal
properties of higher-order programs• Decidability of HOT-PDL model checking of higher-orderprograms via a reduction to higher-order model checking(See the paper for details)• Applications (See the paper for details)• Modeling and extending dependent refinement types• Modeling and extending stack-based access control properties
CAV'18, Oxford, United Kingdom

15

Our Contributions• Higher-Order Trace (HOT) that captures the control flow ofhigher-order programs• Higher-Order Trace Propositional Dynamic Logic (HOT-PDL):• Propositional Dynamic Logic (PDL) over HOTs for specifying temporal
properties of higher-order programs• Decidability of HOT-PDL model checking of higher-orderprograms via a reduction to higher-order model checking(See the paper for details)• Applications (See the paper for details)• Modeling and extending dependent refinement types• Modeling and extending stack-based access control properties
CAV'18, Oxford, United Kingdom

16

Higher-Order Trace (HOT)• A sequence of call and return events equipped with two
kinds of pointers:• Call and return events• call(𝑓𝑓,𝑥𝑥): a call event of the function 𝑓𝑓 with the argument 𝑥𝑥.
• ret(𝑓𝑓, 𝑥𝑥): a return event of the function 𝑓𝑓 with the return value𝑥𝑥.
Inspired by the notion of justification
pointers from the game semantics of PCF• Two kinds of pointers labeled with:• CR : capture the correspondence between call and return events• CC, RC: capture higher-order control flow involving a functionthat is passed to or returned by a higher-order function
CAV'18, Oxford, United Kingdom

17

Higher-Order Trace (HOT)• A sequence of call and return events equipped with two
kinds of pointers:• Call and return events• call(𝑓𝑓,𝑥𝑥): a call event of the function 𝑓𝑓 with the argument 𝑥𝑥.
• ret(𝑓𝑓, 𝑥𝑥): a return event of the function 𝑓𝑓 with the return value𝑥𝑥.
Inspired by the notion of justification
pointers from the game semantics of PCF• Two kinds of pointers labeled with:• CR : capture the correspondence between call and return events• CC, RC: capture higher-order control flow involving a functionthat is passed to or returned by a higher-order function
CAV'18, Oxford, United Kingdom

17

Higher-Order Trace (HOT)• A sequence of call and return events equipped with two
kinds of pointers:• Call and return events• call(𝑓𝑓,𝑥𝑥): a call event of the function 𝑓𝑓 with the argument 𝑥𝑥.
• ret(𝑓𝑓, 𝑥𝑥): a return event of the function 𝑓𝑓 with the return value𝑥𝑥.
Inspired by the notion of justification
pointers from the game semantics of PCF• Two kinds of pointers labeled with:• CR : capture the correspondence between call and return events• CC, RC: capture higher-order control flow involving a functionthat is passed to or returned by a higher-order function
CAV'18, Oxford, United Kingdom

17

Higher-Order Trace (HOT)• A sequence of call and return events equipped with two
kinds of pointers:• Call and return events• call(𝑓𝑓,𝑥𝑥): a call event of the function 𝑓𝑓 with the argument 𝑥𝑥.
• ret(𝑓𝑓, 𝑥𝑥): a return event of the function 𝑓𝑓 with the return value𝑥𝑥.
Inspired by the notion of justification
pointers from the game semantics of PCF• Two kinds of pointers labeled with:• CR : capture the correspondence between call and return events• CC, RC: capture higher-order control flow involving a functionthat is passed to or returned by a higher-order function
CAV'18, Oxford, United Kingdom

17

Higher-Order Trace (HOT)• A sequence of call and return events equipped with two
kinds of pointers:• Call and return events• call(𝑓𝑓,𝑥𝑥): a call event of the function 𝑓𝑓 with the argument 𝑥𝑥.
• ret(𝑓𝑓, 𝑥𝑥): a return event of the function 𝑓𝑓 with the return value𝑥𝑥.
Inspired by the notion of justification
pointers from the game semantics of PCF• Two kinds of pointers labeled with:• CR : capture the correspondence between call and return events• CC, RC: capture higher-order control flow involving a functionthat is passed to or returned by a higher-order function
CAV'18, Oxford, United Kingdom

17

Higher-Order Trace (HOT)• A sequence of call and return events equipped with two
kinds of pointers:• Call and return events• call(𝑓𝑓,𝑥𝑥): a call event of the function 𝑓𝑓 with the argument 𝑥𝑥.
• ret(𝑓𝑓, 𝑥𝑥): a return event of the function 𝑓𝑓 with the return value𝑥𝑥.
Inspired by the notion of justification
pointers from the game semantics of PCF• Two kinds of pointers labeled with:• CR : capture the correspondence between call and return events• CC, RC: capture higher-order control flow involving a functionthat is passed to or returned by a higher-order function
CAV'18, Oxford, United Kingdom

17

Example: Event sequence of 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎
𝐭𝐭𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎→ (𝛌𝛌𝛌𝛌. 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝐱𝐱)) 𝟎𝟎→ 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎)→∗ 𝐢𝐢𝐢𝐢𝐢𝐢 𝟏𝟏 →∗ 𝟐𝟐

CAV'18, Oxford, United Kingdom

18

Example: Event sequence of 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎

𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭, ●𝐭𝐭𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎→ (𝛌𝛌𝛌𝛌. 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝐱𝐱)) 𝟎𝟎→ 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎)→∗ 𝐢𝐢𝐢𝐢𝐢𝐢 𝟏𝟏 →∗ 𝟐𝟐

CAV'18, Oxford, United Kingdom

19

Example: Event sequence of 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎
The function passed
to a higher-orderfunction
𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭, ●𝐭𝐭𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎→ (𝛌𝛌𝛌𝛌. 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝐱𝐱)) 𝟎𝟎→ 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎)→∗ 𝐢𝐢𝐢𝐢𝐢𝐢 𝟏𝟏 →∗ 𝟐𝟐

CAV'18, Oxford, United Kingdom

19

Example: Event sequence of 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎
𝐭𝐭𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎→ (𝛌𝛌𝛌𝛌. 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝐱𝐱)) 𝟎𝟎→ 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎)→∗ 𝐢𝐢𝐢𝐢𝐢𝐢 𝟏𝟏 →∗ 𝟐𝟐

call twice, ● 𝐫𝐫𝐫𝐫𝐫𝐫 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭, ●CAV'18, Oxford, United Kingdom

20

Example: Event sequence of 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎
𝐭𝐭𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎→ (𝛌𝛌𝛌𝛌. 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝐱𝐱)) 𝟎𝟎→ 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎)→∗ 𝐢𝐢𝐢𝐢𝐢𝐢 𝟏𝟏 →∗ 𝟐𝟐

call twice, ● 𝐫𝐫𝐫𝐫𝐫𝐫 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭, ●The function
returned by ahigher-order function

CAV'18, Oxford, United Kingdom

20

Example: Event sequence of 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎
𝐭𝐭𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎→ (𝛌𝛌𝛌𝛌. 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝐱𝐱)) 𝟎𝟎→ 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎)→∗ 𝐢𝐢𝐢𝐢𝐢𝐢 𝟏𝟏 →∗ 𝟐𝟐

call twice, ● ret twice, ● 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 ●, 𝟎𝟎

CAV'18, Oxford, United Kingdom

21

Example: Event sequence of 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎
𝐭𝐭𝐰𝐰𝐰𝐰𝐰𝐰𝐰𝐰 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎→ (𝛌𝛌𝛌𝛌. 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝐱𝐱)) 𝟎𝟎→ 𝐢𝐢𝐢𝐢𝐢𝐢 (𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎)→∗ 𝐢𝐢𝐢𝐢𝐢𝐢 𝟏𝟏 →∗ 𝟐𝟐

call twice, ● ret twice, ● call ●, 0 call ●, 0
call inc, 0 ret inc, 1 ret ●, 1 call ●, 1
call inc, 1 ret inc, 2 ret ●, 2 ret(●, 2)
CAV'18, Oxford, United Kingdom

22

Example: HOT that models the
reduction sequence of 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎
call twice, ●ret twice, ●call ●, 0
call ●, 0
call inc, 0
ret inc, 1
ret ●, 1call ●, 1
call inc, 1
ret inc, 2
ret ●, 2ret(●, 2)

CAV'18, Oxford, United Kingdom

23

Example: HOT that models the
reduction sequence of 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎
CR

Correspondence between
call and return eventsCR

call twice, ●ret twice, ●call ●, 0
call ●, 0
call inc, 0
ret inc, 1
ret ●, 1call ●, 1
call inc, 1
ret inc, 2
ret ●, 2ret(●, 2)

CAV'18, Oxford, United Kingdom

24

Example: HOT that models the
reduction sequence of 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝐢𝐢𝐢𝐢𝐢𝐢 𝟎𝟎
CR

Correspondence between
call and return eventsCR

call twice, ●ret twice, ●call ●, 0
call ●, 0
call inc, 0
ret inc, 1
ret ●, 1call ●, 1
call inc, 1
ret inc, 2
ret ●, 2ret(●, 2)

CC

RC

CC

CAV'18, Oxford, United Kingdom

Higher-order control
flow
CC : call of thefunction passed to ahigher-orderfunction
RC : call of thefunction returned bya higher-orderfunction25

Our Contributions• Higher-Order Trace (HOT) that captures the control flow ofhigher-order programs• Higher-Order Trace Propositional Dynamic Logic (HOT-PDL):• Propositional Dynamic Logic (PDL) over HOTs for specifying temporal
properties of higher-order programs• Decidability of HOT-PDL model checking of higher-orderprograms via a reduction to higher-order model checking(See the paper for details)• Applications (See the paper for details)• Modeling and extending dependent refinement types• Modeling and extending stack-based access control properties
CAV'18, Oxford, United Kingdom

26

Higher-Order Propositional Dynamic Logic(HOT-PDL)• To traverse the pointers, HOT-PDL extends PDL with new pathexpressions (→𝒓𝒓𝒓𝒓𝒓𝒓 ,→𝒄𝒄𝒄𝒄𝒄𝒄𝒄𝒄 )• Each node of a HOT is assigned a truth value indicating whether
the given formula is satisfied• Syntax:• (Formulas)𝝓𝝓 ∷= 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝒕𝒕𝟏𝟏 , 𝒕𝒕𝟐𝟐 𝐫𝐫𝐫𝐫𝐫𝐫 𝒕𝒕𝟏𝟏 , 𝒕𝒕𝟐𝟐 …

• (Path expression)𝝅𝝅 𝝓𝝓 𝝅𝝅 𝝓𝝓

𝝅𝝅 ∷=→ →𝒓𝒓𝒓𝒓𝒓𝒓 →𝒄𝒄𝒄𝒄𝒄𝒄𝒄𝒄 | 𝝅𝝅𝟏𝟏 ⋅ 𝝅𝝅𝟐𝟐 𝝅𝝅𝟏𝟏 + 𝝅𝝅𝟐𝟐 | 𝝅𝝅∗ 𝜙𝜙 ?
CAV'18, Oxford, United Kingdom

27

Higher-Order Propositional Dynamic Logic(HOT-PDL)• To traverse the pointers, HOT-PDL extends PDL with new pathexpressions (→𝒓𝒓𝒓𝒓𝒓𝒓 ,→𝒄𝒄𝒄𝒄𝒄𝒄𝒄𝒄 )• Each node of a HOT is assigned a truth value indicating whether
the given formula is satisfied
Any of top-level functions 𝑓𝑓, bounded integers• Syntax:• (Formulas)𝒏𝒏 ∈ ℤ𝒃𝒃 , or anonymous functions ●𝝓𝝓 ∷= 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝒕𝒕𝟏𝟏 , 𝒕𝒕𝟐𝟐 𝐫𝐫𝐫𝐫𝐫𝐫 𝒕𝒕𝟏𝟏 , 𝒕𝒕𝟐𝟐 …

• (Path expression)𝝅𝝅 𝝓𝝓 𝝅𝝅 𝝓𝝓

𝝅𝝅 ∷=→ →𝒓𝒓𝒓𝒓𝒓𝒓 →𝒄𝒄𝒄𝒄𝒄𝒄𝒄𝒄 | 𝝅𝝅𝟏𝟏 ⋅ 𝝅𝝅𝟐𝟐 𝝅𝝅𝟏𝟏 + 𝝅𝝅𝟐𝟐 | 𝝅𝝅∗ 𝜙𝜙 ?
CAV'18, Oxford, United Kingdom

27

Higher-Order Propositional Dynamic Logic(HOT-PDL)• To traverse the pointers, HOT-PDL extends PDL with new pathexpressions (→𝒓𝒓𝒓𝒓𝒓𝒓 ,→𝒄𝒄𝒄𝒄𝒄𝒄𝒄𝒄 )• Each node of a HOT is assigned a truth value indicating whether
the given formula is satisfied
A call event of a function 𝒕𝒕𝟏𝟏 with an argument 𝒕𝒕𝟐𝟐
• Syntax:• (Formulas)𝝓𝝓 ∷= 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝒕𝒕𝟏𝟏 , 𝒕𝒕𝟐𝟐 𝐫𝐫𝐫𝐫𝐫𝐫 𝒕𝒕𝟏𝟏 , 𝒕𝒕𝟐𝟐 …

• (Path expression)𝝅𝝅 𝝓𝝓 𝝅𝝅 𝝓𝝓

𝝅𝝅 ∷=→ →𝒓𝒓𝒓𝒓𝒓𝒓 →𝒄𝒄𝒄𝒄𝒄𝒄𝒄𝒄 | 𝝅𝝅𝟏𝟏 ⋅ 𝝅𝝅𝟐𝟐 𝝅𝝅𝟏𝟏 + 𝝅𝝅𝟐𝟐 | 𝝅𝝅∗ 𝜙𝜙 ?
CAV'18, Oxford, United Kingdom

28

Higher-Order Propositional Dynamic Logic(HOT-PDL)• To traverse the pointers, HOT-PDL extends PDL with new pathexpressions (→𝒓𝒓𝒓𝒓𝒓𝒓 ,→𝒄𝒄𝒄𝒄𝒄𝒄𝒄𝒄 )• Each node of a HOT is assigned a truth value indicating whether
the given formula is satisfied• Syntax: A return event of a function 𝒕𝒕𝟏𝟏 with a return value 𝒕𝒕𝟐𝟐
• (Formulas)𝝓𝝓 ∷= 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝒕𝒕𝟏𝟏 , 𝒕𝒕𝟐𝟐 𝐫𝐫𝐫𝐫𝐫𝐫 𝒕𝒕𝟏𝟏 , 𝒕𝒕𝟐𝟐 …

• (Path expression)𝝅𝝅 𝝓𝝓 𝝅𝝅 𝝓𝝓

𝝅𝝅 ∷=→ →𝒓𝒓𝒓𝒓𝒓𝒓 →𝒄𝒄𝒄𝒄𝒄𝒄𝒄𝒄 | 𝝅𝝅𝟏𝟏 ⋅ 𝝅𝝅𝟐𝟐 𝝅𝝅𝟏𝟏 + 𝝅𝝅𝟐𝟐 | 𝝅𝝅∗ 𝜙𝜙 ?
CAV'18, Oxford, United Kingdom

29

Higher-Order Propositional Dynamic Logic(HOT-PDL)• To traverse the pointers, HOT-PDL extends PDL with new pathexpressions (→𝒓𝒓𝒓𝒓𝒓𝒓 ,→𝒄𝒄𝒄𝒄𝒄𝒄𝒄𝒄 )• Each node of a HOT is assigned a truth value indicating whether
the given formula is satisfied
Box: 𝜙𝜙 holds at every node reached by the• Syntax:
path represented by 𝜋𝜋• (Formulas)𝝓𝝓 ∷= 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝒕𝒕𝟏𝟏 , 𝒕𝒕𝟐𝟐 𝐫𝐫𝐫𝐫𝐫𝐫 𝒕𝒕𝟏𝟏 , 𝒕𝒕𝟐𝟐 …

• (Path expression)𝝅𝝅 𝝓𝝓 𝝅𝝅 𝝓𝝓

𝝅𝝅 ∷=→ →𝒓𝒓𝒓𝒓𝒓𝒓 →𝒄𝒄𝒄𝒄𝒄𝒄𝒄𝒄 | 𝝅𝝅𝟏𝟏 ⋅ 𝝅𝝅𝟐𝟐 𝝅𝝅𝟏𝟏 + 𝝅𝝅𝟐𝟐 | 𝝅𝝅∗ 𝜙𝜙 ?
CAV'18, Oxford, United Kingdom

30

Higher-Order Propositional Dynamic Logic(HOT-PDL)• To traverse the pointers, HOT-PDL extends PDL with new pathexpressions (→𝒓𝒓𝒓𝒓𝒓𝒓 ,→𝒄𝒄𝒄𝒄𝒄𝒄𝒄𝒄 )• Each node of a HOT is assigned a truth value indicating whether
the given formula is satisfied
Diamond: there exists a node that can be• Syntax:
reached by 𝜋𝜋 and 𝜙𝜙 holds• (Formulas)𝝓𝝓 ∷= 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝒕𝒕𝟏𝟏 , 𝒕𝒕𝟐𝟐 𝐫𝐫𝐫𝐫𝐫𝐫 𝒕𝒕𝟏𝟏 , 𝒕𝒕𝟐𝟐 …

• (Path expression)𝝅𝝅 𝝓𝝓 𝝅𝝅 𝝓𝝓

𝝅𝝅 ∷=→ →𝒓𝒓𝒓𝒓𝒓𝒓 →𝒄𝒄𝒄𝒄𝒄𝒄𝒄𝒄 | 𝝅𝝅𝟏𝟏 ⋅ 𝝅𝝅𝟐𝟐 𝝅𝝅𝟏𝟏 + 𝝅𝝅𝟐𝟐 | 𝝅𝝅∗ 𝜙𝜙 ?
CAV'18, Oxford, United Kingdom

31

Higher-Order Propositional Dynamic Logic(HOT-PDL)• To traverse the pointers, HOT-PDL extends PDL with new pathexpressions (→𝒓𝒓𝒓𝒓𝒓𝒓 ,→𝒄𝒄𝒄𝒄𝒄𝒄𝒄𝒄 )• Each node of a HOT is assigned a truth value indicating whether
the given formula is satisfied• Syntax:• (Formulas)𝝓𝝓 ∷= 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝒕𝒕𝟏𝟏 , 𝒕𝒕𝟐𝟐 𝐫𝐫𝐫𝐫𝐫𝐫 𝒕𝒕𝟏𝟏 , 𝒕𝒕𝟐𝟐 …

• (Path expression)𝝅𝝅 𝝓𝝓 𝝅𝝅 𝝓𝝓

𝝅𝝅 ∷=→ →𝒓𝒓𝒓𝒓𝒓𝒓 →𝒄𝒄𝒄𝒄𝒄𝒄𝒄𝒄 | 𝝅𝝅𝟏𝟏 ⋅ 𝝅𝝅𝟐𝟐 𝝅𝝅𝟏𝟏 + 𝝅𝝅𝟐𝟐 | 𝝅𝝅∗ 𝜙𝜙 ?

Concatenation

alternation

CAV'18, Oxford, United Kingdom

Kleene star32

Higher-Order Propositional Dynamic Logic(HOT-PDL)• To traverse the pointers, HOT-PDL extends PDL with new pathexpressions (→𝒓𝒓𝒓𝒓𝒓𝒓 ,→𝒄𝒄𝒄𝒄𝒄𝒄𝒄𝒄 )• Each node of a HOT is assigned a truth value indicating whether
the given formula is satisfied• Syntax:• (Formulas)𝝓𝝓 ∷= 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝒕𝒕𝟏𝟏 , 𝒕𝒕𝟐𝟐 𝐫𝐫𝐫𝐫𝐫𝐫 𝒕𝒕𝟏𝟏 , 𝒕𝒕𝟐𝟐 …

• (Path expression)𝝅𝝅 𝝓𝝓 𝝅𝝅 𝝓𝝓

𝝅𝝅 ∷=→ →𝒓𝒓𝒓𝒓𝒓𝒓 →𝒄𝒄𝒄𝒄𝒄𝒄𝒄𝒄 | 𝝅𝝅𝟏𝟏 ⋅ 𝝅𝝅𝟐𝟐 𝝅𝝅𝟏𝟏 + 𝝅𝝅𝟐𝟐 | 𝝅𝝅∗ 𝜙𝜙 ?
tests if 𝜙𝜙 holds at the current node
CAV'18, Oxford, United Kingdom

33

Higher-Order Propositional Dynamic Logic(HOT-PDL)• To traverse the pointers, HOT-PDL extends PDL with new pathexpressions (→𝒓𝒓𝒓𝒓𝒓𝒓 ,→𝒄𝒄𝒄𝒄𝒄𝒄𝒄𝒄 )• Each node of a HOT is assigned a truth value indicating whether
the given formula is satisfied• Syntax:• (Formulas)𝝓𝝓 ∷= 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝒕𝒕𝟏𝟏 , 𝒕𝒕𝟐𝟐 𝐫𝐫𝐫𝐫𝐫𝐫 𝒕𝒕𝟏𝟏 , 𝒕𝒕𝟐𝟐 …

• (Path expression)𝝅𝝅 𝝓𝝓 𝝅𝝅 𝝓𝝓

𝝅𝝅 ∷=→ →𝒓𝒓𝒓𝒓𝒓𝒓 →𝒄𝒄𝒄𝒄𝒄𝒄𝒄𝒄 | 𝝅𝝅𝟏𝟏 ⋅ 𝝅𝝅𝟐𝟐 𝝅𝝅𝟏𝟏 + 𝝅𝝅𝟐𝟐 | 𝝅𝝅∗ 𝜙𝜙 ?

move to the next event in the sequence
CAV'18, Oxford, United Kingdom

34

Higher-Order Propositional Dynamic Logic(HOT-PDL)• To traverse the pointers, HOT-PDL extends PDL with new pathexpressions (→𝒓𝒓𝒓𝒓𝒓𝒓 ,→𝒄𝒄𝒄𝒄𝒄𝒄𝒄𝒄 )• Each node of a HOT is assigned a truth value indicating whether
the given formula is satisfied• Syntax:• (Formulas)𝝓𝝓 ∷= 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝒕𝒕𝟏𝟏 , 𝒕𝒕𝟐𝟐 𝐫𝐫𝐫𝐫𝐫𝐫 𝒕𝒕𝟏𝟏 , 𝒕𝒕𝟐𝟐 …

• (Path expression)𝝅𝝅 𝝓𝝓 𝝅𝝅 𝝓𝝓

𝝅𝝅 ∷=→ →𝒓𝒓𝒓𝒓𝒓𝒓 →𝒄𝒄𝒄𝒄𝒄𝒄𝒄𝒄 | 𝝅𝝅𝟏𝟏 ⋅ 𝝅𝝅𝟐𝟐 𝝅𝝅𝟏𝟏 + 𝝅𝝅𝟐𝟐 | 𝝅𝝅∗ 𝜙𝜙 ?
CAV'18, Oxford, United Kingdom

35

Higher-Order Propositional Dynamic Logic(HOT-PDL)• To traverse the pointers, HOT-PDL extends PDL with new pathexpressions (→𝒓𝒓𝒓𝒓𝒓𝒓 ,→𝒄𝒄𝒄𝒄𝒄𝒄𝒄𝒄 )• Each node of a HOT is assigned a truth value indicating whether
the given formula is satisfied• Syntax:• (Formulas)𝝓𝝓 ∷= 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝒕𝒕𝟏𝟏 , 𝒕𝒕𝟐𝟐 𝐫𝐫𝐫𝐫𝐫𝐫 𝒕𝒕𝟏𝟏 , 𝒕𝒕𝟐𝟐 …

• (Path expression)𝝅𝝅 𝝓𝝓 𝝅𝝅 𝝓𝝓

𝝅𝝅 ∷=→ →𝒓𝒓𝒓𝒓𝒓𝒓 →𝒄𝒄𝒄𝒄𝒄𝒄𝒄𝒄 | 𝝅𝝅𝟏𝟏 ⋅ 𝝅𝝅𝟐𝟐 𝝅𝝅𝟏𝟏 + 𝝅𝝅𝟐𝟐 | 𝝅𝝅∗ 𝜙𝜙 ?
traverse an edge labeled with CR
CAV'18, Oxford, United Kingdom

36

Higher-Order Propositional Dynamic Logic(HOT-PDL)• To traverse the pointers, HOT-PDL extends PDL with new pathexpressions (→𝒓𝒓𝒓𝒓𝒓𝒓 ,→𝒄𝒄𝒄𝒄𝒄𝒄𝒄𝒄 )• Each node of a HOT is assigned a truth value indicating whether
the given formula is satisfied• Syntax:• (Formulas)𝝓𝝓 ∷= 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝒕𝒕𝟏𝟏 , 𝒕𝒕𝟐𝟐 𝐫𝐫𝐫𝐫𝐫𝐫 𝒕𝒕𝟏𝟏 , 𝒕𝒕𝟐𝟐 …

• (Path expression)𝝅𝝅 𝝓𝝓 𝝅𝝅 𝝓𝝓

𝝅𝝅 ∷=→ →𝒓𝒓𝒓𝒓𝒓𝒓 →𝒄𝒄𝒄𝒄𝒄𝒄𝒄𝒄 | 𝝅𝝅𝟏𝟏 ⋅ 𝝅𝝅𝟐𝟐 𝝅𝝅𝟏𝟏 + 𝝅𝝅𝟐𝟐 | 𝝅𝝅∗ 𝜙𝜙 ?
traverse an edge labeled with CC or RC
CAV'18, Oxford, United Kingdom

37

Example : The property that cannot be
expressed by the previous specification
languages

If the function returned by a partial application of twice tosome function is called with some integer n, then the function
argument passed to twice is eventually called with n∗→ � 𝒙𝒙 ∈ ℤ𝒃𝒃

𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭,� ∧ →𝐫𝐫𝐫𝐫𝐫𝐫 ⋅→𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙⇒ →𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙
CAV'18, Oxford, United Kingdom

38

Example : The property that cannot be
expressed by the previous specification
languages

If the function returned by a partial application of twice tosome function is called with some integer n, then the function
argument passed to twice is eventually called with n∗→ � 𝒙𝒙 ∈ ℤ𝒃𝒃

𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭,� ∧ →𝐫𝐫𝐫𝐫𝐫𝐫 ⋅→𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙⇒ →𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙ℤ𝒃𝒃 : bounded
integers

CAV'18, Oxford, United Kingdom

38

Example : The property that cannot be
expressed by the previous specification
languages

If the function returned by a partial application of twice tosome function is called with some integer n, then the function
argument passed to twice is eventually called with n∗→ � 𝒙𝒙 ∈ ℤ𝒃𝒃→∗ 𝝓𝝓 = 𝐆𝐆𝝓𝝓(in LTL)

𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭,� ∧ →𝐫𝐫𝐫𝐫𝐫𝐫 ⋅→𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙⇒ →𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙ℤ𝒃𝒃 : bounded
integers

CAV'18, Oxford, United Kingdom

38

Example : The property that cannot be
expressed by the previous specification
languages

If the function returned by a partial application of twice tosome function is called with some integer n, then the function
argument passed to twice is eventually called with n∗→ � 𝒙𝒙 ∈ ℤ𝒃𝒃

𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭,� ∧ →𝐫𝐫𝐫𝐫𝐫𝐫 ⋅→𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙⇒ →𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙

Globally, for all bounded integer x,
CAV'18, Oxford, United Kingdom

39

Example : The property that cannot be
expressed by the previous specification
languages

If the function returned by a partial application of twice tosome function is called with some integer n, then the function
argument passed to twice is eventually called with n∗→ � 𝒙𝒙 ∈ ℤ𝒃𝒃

𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭,� ∧ →𝐫𝐫𝐫𝐫𝐫𝐫 ⋅→𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙⇒ →𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙

If the function twice is called
CAV'18, Oxford, United Kingdom

40

Example : The property that cannot be
expressed by the previous specification
languages

If the function returned by a partial application of twice tosome function is called with some integer n, then the function
argument passed to twice is eventually called with n∗→ � 𝒙𝒙 ∈ ℤ𝒃𝒃

𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭,� ∧ →𝐫𝐫𝐫𝐫𝐫𝐫 ⋅→𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙⇒ →𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙

and the function returned by twice is called withan argument x,
CAV'18, Oxford, United Kingdom

41

Example : The property that cannot be
expressed by the previous specification
languages

If the function returned by a partial application of twice tosome function is called with some integer n, then the function
argument passed to twice is eventually called with n∗→ � 𝒙𝒙 ∈ ℤ𝒃𝒃

𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭,� ∧ →𝐫𝐫𝐫𝐫𝐫𝐫 ⋅→𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙⇒ →𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙then the function argument passed to twice is eventuallycalled with the argument x
CAV'18, Oxford, United Kingdom

42

Example : The property that cannot be
expressed by the previous specificationCClanguages
call twice, ●CR→∗� 𝒙𝒙 ∈ ℤ𝒃𝒃

𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭,� ∧ →𝐫𝐫𝐫𝐫𝐫𝐫 ⋅→𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙⇒ →𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙

The formula holds at
the node labeled withthe event call twice, ●CR

CAV'18, Oxford, United Kingdom

ret twice, ●call ●, 0
call ●, 0
call inc, 0
ret inc, 1
ret ●, 1call ●, 1
call inc, 1
ret inc, 2
ret ●, 2ret(●, 2)

RC

CC

43

Example : The property that cannot be
expressed by the previous specificationCClanguages
call twice, ●CR→∗� 𝒙𝒙 ∈ ℤ𝒃𝒃

𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭,� ∧ →𝐫𝐫𝐫𝐫𝐫𝐫 ⋅→𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙⇒ →𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙

The formula holds at
the node labeled withthe event call twice, ●CR

CAV'18, Oxford, United Kingdom

ret twice, ●call ●, 0
call ●, 0
call inc, 0
ret inc, 1
ret ●, 1call ●, 1
call inc, 1
ret inc, 2
ret ●, 2ret(●, 2)

RC

CC

44

Example : The property that cannot be
expressed by the previous specificationCClanguages
call twice, ●CR→∗� 𝒙𝒙 ∈ ℤ𝒃𝒃

𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭,� ∧ →𝐫𝐫𝐫𝐫𝐫𝐫 ⋅→𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙⇒ →𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙

The formula holds at
the node labeled withthe event call twice, ●CR

CAV'18, Oxford, United Kingdom

ret twice, ●call ●, 0
call ●, 0
call inc, 0
ret inc, 1
ret ●, 1call ●, 1
call inc, 1
ret inc, 2
ret ●, 2ret(●, 2)

RC

CC

45

Example : The property that cannot be
expressed by the previous specificationCClanguages
call twice, ●CR→∗� 𝒙𝒙 ∈ ℤ𝒃𝒃

𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭,� ∧ →𝐫𝐫𝐫𝐫𝐫𝐫 ⋅→𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙⇒ →𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙

The formula holds at
the node labeled withthe event call twice, ●CR

CAV'18, Oxford, United Kingdom

ret twice, ●call ●, 0
call ●, 0
call inc, 0
ret inc, 1
ret ●, 1call ●, 1
call inc, 1
ret inc, 2
ret ●, 2ret(●, 2)

RC

CC

46

Example : The property that cannot be
expressed by the previous specificationCClanguages
call twice, ●CR

𝒙𝒙 = 𝟎𝟎→∗

� 𝒙𝒙 ∈ ℤ𝒃𝒃

𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭,� ∧ →𝐫𝐫𝐫𝐫𝐫𝐫 ⋅→𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙⇒ →𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙

The formula holds at
the node labeled withthe event call twice, ●CR

CAV'18, Oxford, United Kingdom

ret twice, ●call ●, 0
call ●, 0
call inc, 0
ret inc, 1
ret ●, 1call ●, 1
call inc, 1
ret inc, 2
ret ●, 2ret(●, 2)

RC

CC

47

Example : The property that cannot be
expressed by the previous specificationCClanguages
call twice, ●CR

𝒙𝒙 = 𝟎𝟎→∗

� 𝒙𝒙 ∈ ℤ𝒃𝒃

𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭,� ∧ →𝐫𝐫𝐫𝐫𝐫𝐫 ⋅→𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙⇒ →𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙

The formula holds at
the node labeled withthe event call twice, ●CR

CAV'18, Oxford, United Kingdom

ret twice, ●call ●, 0
call ●, 0
call inc, 0
ret inc, 1
ret ●, 1call ●, 1
call inc, 1
ret inc, 2
ret ●, 2ret(●, 2)

RC

CC

48

Example : The property that cannot be
expressed by the previous specificationCClanguages
call twice, ●CR

𝒙𝒙 = 𝟎𝟎→∗

� 𝒙𝒙 ∈ ℤ𝒃𝒃

𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭,� ∧ →𝐫𝐫𝐫𝐫𝐫𝐫 ⋅→𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙⇒ →𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 𝐜𝐜𝐜𝐜𝐜𝐜𝐜𝐜 �, 𝒙𝒙

The formula holds at
the node labeled withthe event call twice, ●𝒙𝒙 = 𝟎𝟎
CAV'18, Oxford, United KingdomCR

ret twice, ●call ●, 0
call ●, 0
call inc, 0
ret inc, 1
ret ●, 1call ●, 1
call inc, 1
ret inc, 2
ret ●, 2ret(●, 2)

RC

CC

49

Conclusion• HOT captures the control flow of higher-order programs• HOT-PDL is an extension of PDL defined over HOTs

• Enables a precise specification of temporal trace properties for higherorder programs• Provides a foundation for specification in various application domains• stack-based access control properties• dependent refinement types• HOT-PDL model checking of higher-order programs is shown
decidable via a reduction to higher-order model checking• Future work: extend HOTs with new kinds of events andpointers for capturing call-by-name and/or effectful
computations by incorporating more ideas from game semantics
CAV'18, Oxford, United Kingdom

50