1 citations · 1 across the 5 of their papers we have counts for
10 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…
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 lexi…
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…
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…