Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Denotational Product Construction for Temporal Verification of Effectful Higher-Order Programs

Kazuki Watanabe, Mayuko Kori, Taro Sekiyama, Satoshi Kura, Hiroshi Unno

TL;DR

This work presents a denotational product construction that reduces linear-time temporal verification of effectful higher-order programs, including probabilistic ones, to non-temporal weakest-precondition problems. It combines a synchronisation step via strong monad morphisms with a store-passing style (SPS) transformation to produce a product program whose wp corresponds to the original temporal property. Correctness is established through a fibrational logical-relations framework and extended to recursive (fixpoint) definitions. The approach is instantiated for probabilistic and angelic nondeterministic programs, and an automated verifier for the probabilistic case is demonstrated on several benchmarks using an existing solver. This method enables modular, solver-friendly verification of complex higher-order programs with recursion and effects, with potential extensions to non-terminating traces and continuous distributions.

Abstract

We propose a categorical framework for linear-time temporal verification of effectful higher-order programs, including probabilistic higher-order programs. Our framework provides a generic denotational reduction -- namely, a denotational product construction -- from linear-time safety verification of effectful higher-order programs to computation of weakest pre-conditions of product programs. This reduction enables us to apply existing algorithms for such well-studied computations of weakest pre-conditions, some of which are available as off-the-shelf solvers. We show the correctness of our denotational product construction by proving a preservation theorem under strong monad morphisms and an existence of suitable liftings along a fibration. We instantiate our framework with both probabilistic and angelic nondeterministic higher-order programs, and implement an automated solver for the probabilistic case based on the existing solver developed by Kura and Unno. To the best of our knowledge, this is the first automated verifier for linear-time temporal verification of probabilistic higher-order programs with recursion.

A Denotational Product Construction for Temporal Verification of Effectful Higher-Order Programs

TL;DR

This work presents a denotational product construction that reduces linear-time temporal verification of effectful higher-order programs, including probabilistic ones, to non-temporal weakest-precondition problems. It combines a synchronisation step via strong monad morphisms with a store-passing style (SPS) transformation to produce a product program whose wp corresponds to the original temporal property. Correctness is established through a fibrational logical-relations framework and extended to recursive (fixpoint) definitions. The approach is instantiated for probabilistic and angelic nondeterministic programs, and an automated verifier for the probabilistic case is demonstrated on several benchmarks using an existing solver. This method enables modular, solver-friendly verification of complex higher-order programs with recursion and effects, with potential extensions to non-terminating traces and continuous distributions.

Abstract

We propose a categorical framework for linear-time temporal verification of effectful higher-order programs, including probabilistic higher-order programs. Our framework provides a generic denotational reduction -- namely, a denotational product construction -- from linear-time safety verification of effectful higher-order programs to computation of weakest pre-conditions of product programs. This reduction enables us to apply existing algorithms for such well-studied computations of weakest pre-conditions, some of which are available as off-the-shelf solvers. We show the correctness of our denotational product construction by proving a preservation theorem under strong monad morphisms and an existence of suitable liftings along a fibration. We instantiate our framework with both probabilistic and angelic nondeterministic higher-order programs, and implement an automated solver for the probabilistic case based on the existing solver developed by Kura and Unno. To the best of our knowledge, this is the first automated verifier for linear-time temporal verification of probabilistic higher-order programs with recursion.

Paper Structure

This paper contains 49 sections, 31 theorems, 64 equations, 3 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Overview
  3. Temporal Verification Problem of Probabilistic Programs
  4. Synchronisation
  5. SPS Transformation
  6. Notation.
  7. Source Program: $\lambda_c$-Calculus with Generic Effects
  8. Syntax
  9. Syntax Sugar.
  10. Semantics and Weakest Precondition
  11. Synchronisation of $\lambda_c$-Calculus with Specifications
  12. Translation of Effectful Programs by Strong Monad Morphisms
  13. Generic Framework for Synchronisations
  14. SPS Transformation of $\lambda_c$-Calculus
  15. Recursion
  16. ...and 34 more sections

Key Result

lemma 1

Let $\alpha\colon T\Rightarrow U$ be a strong monad morphism. For each well-typed $\lambda_c$-term $x_1\colon \mathbf{t}_1,\dots, x_n\colon \mathbf{t}_n\vdash M\colon \mathbf{t}$, where $\mathbf{t}_1, \dots, \mathbf{t}_n, \mathbf{t}$ are ground types, we have

Figures (3)

  • Figure 1: Outline of our denotational product construction.
  • Figure 2: The SPS transformation for terms.
  • Figure 3: Typing rules of the source program without recursion.

Theorems & Definitions (68)

  • definition 1: $\lambda_c$-signature
  • definition 2: $\lambda_c(\Sigma)$-structure and ${\mathcal{A}\llbracket \_\rrbracket_{T}}$
  • definition 3: weakest pre-condition AguirreKK22
  • definition 4: strong monad morphism
  • definition 5: map of $\lambda_c(\Sigma)$-structure Katsumata13
  • lemma 1: Katsumata13Kura2023
  • definition 6: inference query
  • theorem 1: correctness
  • definition 7: product situation
  • proposition 1
  • ...and 58 more