arXiv subjects

Satoshi Kura

Publications and source records attributed to Satoshi Kura.

14 recordsLinked to original sources

arXiv2026

Solving First-Order Fixed-Point Logics via a Least-to-Greatest Transformation Based on Game Semantics

Fixed-point logics provide an expressive intermediate framework for reasoning about temporal properties of programs. One of the key approaches to solving their validity checking problem is via transformations from least fixed points to greatest fixed points ($\mu$-to-$\nu$ transformations), which generalizes a reduction from termination verification to safety verification studied in binary reachability analysis. In this paper, we introduce game-semantic interpretations of $\mu$-to-$\nu$ transformations. We first introduce a new $\mu$-to-$\nu$ transformation based on parity relations. We show that solving $\mu$-to-$\nu$-transformed fixed-point equation systems corresponds to finding winning strategies in the game semantics of the original fixed-point equation systems. We apply the same game-semantic framework to interpret two existing $\mu$-to-$\nu$ transformations, one by Kobayashi et al.\ and the other by Unno et al, and show that they admit analogous game-semantic interpretations. Furthermore, we show that the game introduced by Tsukada et al.\ corresponds to an alternative characterization of the winning condition. On the implementation side, we propose optimization techniques for efficiently solving our new $\mu$-to-$\nu$ transformation. We implement these techniques in a fixed-point logic solver, compare our approach with existing solvers, and demonstrate the effectiveness of the proposed optimizations through experiments.

cs.LO↗

arXiv2026

Formal Verification of Probing Security via Conditional Independence

Side-channel attacks are a major threat to the security of cryptosystems. Masking is a widely used countermeasure against such attacks, but proving the security of masked algorithms is error-prone without formal verification. In this work, we propose a novel approach to formal verification of noninterference properties of masked algorithms based on probabilistic separation logic. By establishing a connection between noninterference and conditional independence, we show how noninterference can be verified using Lilac, a separation logic for conditional independence. We also provide several proof rules that facilitate the verification of probing security and demonstrate their application to example algorithms.

cs.LO↗

arXiv2026

Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification

Many quantitative properties of probabilistic programs can be characterized as least fixed points, but verifying their lower bounds remains a challenging problem. We present a new approach to lower-bound verification that exploits and extends the connection between the uniqueness of fixed points and program termination. The core technical tool is a generalization of ranking supermartingales, which serves as witnesses of the uniqueness of fixed points. Our method provides a simple and unified reasoning principle applicable to a wide range of quantitative properties, including termination probability, the weakest preexpectation, expected runtime, higher moments of runtime, and conditional weakest preexpectation. We provide a template-based algorithm for automated verification of lower bounds and demonstrate the effectiveness of the proposed method via experiments.

cs.LO↗

arXiv2026

A Hierarchy of Supermartingales for $ω$-Regular Verification

We propose new supermartingale-based certificates for verifying almost sure satisfaction of $ω$-regular properties: (1) generalised Streett supermartingales (GSSMs) and their lexicographic extension (LexGSSMs), (2) distribution-valued Streett supermartingales (DVSSMs), and (3) progress-measure supermartingales (PMSMs) and their lexicographic extension (LexPMSMs). GSSMs, LexGSSMs, and DVSSMs are derived from least-fixed point characterisations of positive recurrence and null recurrence of Markov chains with respect to given Streett conditions; and PMSMs and LexPMSMs are probabilistic extensions of parity progress measures. We study the hierarchy among these certificates and existing certificates, namely Streett supermartingales, by comparing the classes of problems that can be verified by each type of certificates. Notably, we show that our certificates are strictly more powerful than Streett supermartingales. We also prove completeness of GSSMs for positive recurrence and of DVSSMs for null recurrence: DVSSMs are, in theory, the most powerful certificates in the sense that for any Markov chain that almost surely satisfies a given $ω$-regular property, there exists a DVSSM certifying it. We provide a sound and relatively complete algorithm for synthesising LexPMSMs, the second most powerful certificates in the hierarchy. We have implemented a prototype tool based on this algorithm, and our experiments show that our tool can successfully synthesise certificates for various examples including those that cannot be certified by existing supermartingales.

cs.LO↗

arXiv2026

On Complete Categorical Semantics for Effect Handlers

Soundness and completeness with respect to equational theories for programming languages are fundamental properties in the study of categorical semantics. However, completeness results have not been established for programming languages with algebraic effects and handlers, which raises a question of whether the commonly used models in the literature, i.e., free model monads generated from algebraic theories, are the only valid semantic models for effect handlers. In this paper, we show that this is not the case. We identify the precise characterizations of categorical models of effect handlers that allow us to establish soundness and completeness results with respect to a certain equational theory for effect handling constructs. Notably, this allows us to capture not only free monad models but also the CPS semantics for effect handlers as models of the calculus.

cs.LO↗

arXiv2026

A Category-Theoretic Framework for Dependent Effect Systems

Graded monads refine traditional monads using effect annotations in order to describe quantitatively the computational effects that a program can generate. They have been successfully applied to a variety of formal systems for reasoning about effectful computations. However, existing categorical frameworks for graded monads do not support effects that may depend on program values, which we call dependent effects, thereby limiting their expressiveness. We address this limitation by introducing indexed graded monads, a categorical generalization of graded monads inspired by the fibrational "indexed" view and by classical categorical semantics of dependent type theories. We show how indexed graded monads provide semantics for a refinement type system with dependent effects. We also show how this type system can be instantiated with specific choices of parameters to obtain several formal systems for reasoning about specific program properties. These instances include, in particular, cost analysis, probability-bound reasoning, expectation-bound reasoning, and temporal safety verification.

cs.LO↗

arXiv2025

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

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.

cs.LO↗

arXiv2025

Higher-Order Weakest Precondition Transformers via a CPS Transformation

Weakest preconditions are a useful notion for program verification as they reduce a problem of program verification to a problem of constraint solving. Category-theoretic generalisations of weakest preconditions have been studied to capture various computational effects and various properties in a unified framework. In this paper, we propose a novel and general relationship between weakest precondition transformers and CPS transformations for higher-order functional languages with general computational effects and recursion. Technically, this gives a syntactic counterpart of the categorically-defined generic weakest precondition transformer in [Aguirre & Katsumata, 2020]. The usefulness of our results is threefold. (1) Since CPS transformations purify effectful programs, various verification problems for effectful programs can be reduced to verification problems for pure programs. This syntactic reduction makes it easier to solve the verification problems and potentially facilitates combinations with other sophisticated verification methods tailored for pure programs. (2) We capture two existing verification methods, namely, verification of event sequences [Kobayashi et al., 2018] and expected cost [Avanzini et al., 2021] as instances of our framework. (3) Our results streamline the process of extending weakest precondition transformers for imperative programs to those for higher-order programs. We show two such extensions: analysis of higher moments of cost and the conditional weakest pre-expectation for higher-order probabilistic programs. These extensions demonstrate that our theoretical framework can produce novel verification methods.

cs.LO↗

arXiv2025

Logical relations for call-by-push-value models, via internal fibrations in a 2-category

We give a denotational account of logical relations for call-by-push-value (CBPV) in the fibrational style of Hermida, Jacobs, Katsumata and others. Fibrations -- which axiomatise the usual notion of sets-with-relations -- provide a clean framework for constructing new, logical relations-style, models. Such models can then be used to study properties such as effect simulation. Extending this picture to CBPV is challenging: the models incorporate both adjunctions and enrichment, making the appropriate notion of fibration unclear. We handle this using 2-category theory. We identify an appropriate 2-category, and define CBPV fibrations to be fibrations internal to this 2-category which strictly preserve the CBPV semantics. Next, we develop the theory so it parallels the classical setting. We give versions of the codomain and subobject fibrations, and show that new models can be constructed from old ones by pullback. The resulting framework enables the construction of new, logical relations-style, models for CBPV. Finally, we demonstrate the utility of our approach with particular examples. These include a generalisation of Katsumata's $\top\top$-lifting to CBPV models, an effect simulation result, and a relative full completeness result for CBPV without sum types.

cs.LO↗

arXiv2024

Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System

Verification of higher-order probabilistic programs is a challenging problem. We present a verification method that supports several quantitative properties of higher-order probabilistic programs. Usually, extending verification methods to handle the quantitative aspects of probabilistic programs often entails extensive modifications to existing tools, reducing compatibility with advanced techniques developed for qualitative verification. In contrast, our approach necessitates only small amounts of modification, facilitating the reuse of existing techniques and implementations. On the theoretical side, we propose a dependent refinement type system for a generalised higher-order fixed point logic (HFL). Combined with continuation-passing style encodings of properties into HFL, our dependent refinement type system enables reasoning about several quantitative properties, including weakest pre-expectations, expected costs, moments of cost, and conditional weakest pre-expectations for higher-order probabilistic programs with continuous distributions and conditioning. The soundness of our approach is proved in a general setting using a framework of categorical semantics so that we don't have to repeat similar proofs for each individual problem. On the empirical side, we implement a type checker for our dependent refinement type system that reduces the problem of type checking to constraint solving. We introduce admissible predicate variables and integrable predicate variables to constrained Horn clauses (CHC) so that we can soundly reason about the least fixed points and samplings from probability distributions. Our implementation demonstrates that existing CHC solvers developed for non-probabilistic programs can be extended to a solver for the extended CHC with only small efforts. We also demonstrate the ability of our type checker to verify various concrete examples.

cs.LO↗

arXiv2021

Decision Tree Learning in CEGIS-Based Termination Analysis

We present a novel decision tree-based synthesis algorithm of ranking functions for verifying program termination. Our algorithm is integrated into the workflow of CounterExample Guided Inductive Synthesis (CEGIS). CEGIS is an iterative learning model where, at each iteration, (1) a synthesizer synthesizes a candidate solution from the current examples, and (2) a validator accepts the candidate solution if it is correct, or rejects it providing counterexamples as part of the next examples. Our main novelty is in the design of a synthesizer: building on top of a usual decision tree learning algorithm, our algorithm detects cycles in a set of example transitions and uses them for refining decision trees. We have implemented the proposed method and obtained promising experimental results on existing benchmark sets of (non-)termination verification problems that require synthesis of piecewise-defined lexicographic affine ranking functions.

cs.LO↗

arXiv2020

General Semantic Construction of Dependent Refinement Type Systems, Categorically

Refinement types are types equipped with predicates that specify preconditions and postconditions of underlying functional languages. We propose a general semantic construction of dependent refinement type systems from underlying type systems and predicate logic, that is, a construction of liftings of closed comprehension categories from given (underlying) closed comprehension categories and posetal fibrations for predicate logic. We give sufficient conditions to lift structures such as dependent products, dependent sums, computational effects, and recursion from the underlying type systems to refinement type systems. We demonstrate the usage of our construction by giving semantics to a refinement type system and proving soundness.

cs.LO↗

arXiv2020

Graded Algebraic Theories

We provide graded extensions of algebraic theories and Lawvere theories that correspond to graded monads. We prove that graded algebraic theories, graded Lawvere theories, and finitary graded monads are equivalent via equivalence of categories, which extends the equivalence for monads. We also give sums and tensor products of graded algebraic theories to combine computational effects as an example of importing techniques based on algebraic theories to graded monads.

cs.LO↗

arXiv2019

Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments

Programs with randomization constructs is an active research topic, especially after the recent introduction of martingale-based analysis methods for their termination and runtimes. Unlike most of the existing works that focus on proving almost-sure termination or estimating the expected runtime, in this work we study the tail probabilities of runtimes-such as "the execution takes more than 100 steps with probability at most 1%." To this goal, we devise a theory of supermartingales that overapproximate higher moments of runtime. These higher moments, combined with a suitable concentration inequality, yield useful upper bounds of tail probabilities. Moreover, our vector-valued formulation enables automated template-based synthesis of those supermartingales. Our experiments suggest the method's practical use.

cs.LO↗