1 citations · 3 across the 12 of their papers we have counts for
14 papers
Solving First-Order Fixed-Point Logics via a Least-to-Greatest Transformation Based on Game Semantics
Satoshi Kura, Hiroshi Unno
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 pr…
Formal Verification of Probing Security via Conditional Independence
Satoshi Kura, Katsuyuki Takashima
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 algorithm…
On Complete Categorical Semantics for Effect Handlers
Satoshi Kura
Soundness and completeness with respect to equational theories for programming languages are fundamental properties in the study of categorical semantics. However, completeness res…
A Category-Theoretic Framework for Dependent Effect Systems
Satoshi Kura, Marco Gaboardi, Taro Sekiyama +1
Graded monads refine traditional monads using effect annotations in order to describe quantitatively the computational effects that a program can generate. They have been successfu…
A Hierarchy of Supermartingales for -Regular Verification
Satoshi Kura, Hiroshi Unno
We propose new supermartingale-based certificates for verifying almost sure satisfaction of -regular properties: (1) generalised Streett supermartingales (GSSMs) and their lexic…
A Denotational Product Construction for Temporal Verification of Effectful Higher-Order Programs
Kazuki Watanabe, Mayuko Kori, Taro Sekiyama +2
We propose a categorical framework for linear-time temporal verification of effectful higher-order programs, including probabilistic higher-order programs. Our framework provides a…
Logical relations for call-by-push-value models, via internal fibrations in a 2-category
Pedro H. Azevedo de Amorim, Satoshi Kura, Philip Saville
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…
Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification
Satoshi Kura, Hiroshi Unno, Takeshi Tsukada
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…
Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System
Satoshi Kura, Hiroshi Unno
Verification of higher-order probabilistic programs is a challenging problem. We present a verification method that supports several quantitative properties of higher-order probabi…
Higher-Order Weakest Precondition Transformers via a CPS Transformation
Satoshi Kura
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 generalis…
Decision Tree Learning in CEGIS-Based Termination Analysis
Satoshi Kura, Hiroshi Unno, Ichiro Hasuo
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 G…
General Semantic Construction of Dependent Refinement Type Systems, Categorically
Satoshi Kura
Refinement types are types equipped with predicates that specify preconditions and postconditions of underlying functional languages. We propose a general semantic construction of…
Graded Algebraic Theories
Satoshi Kura
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 fini…
Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments
Satoshi Kura, Natsuki Urabe, Ichiro Hasuo
Programs with randomization constructs is an active research topic, especially after the recent introduction of martingale-based analysis methods for their termination and runtimes…