Search Results

Documents authored by Sakayori, Ken

Document
DOI: 10.4230/LIPIcs.CONCUR.2026.43
Prophecy-Based Automated Verification of Message-Passing Programs

Authors: Takashi Nagatomi, Musashi Katsura, Naoki Kobayashi, Yusuke Matsushita, and Ken Sakayori

Published in: LIPIcs, Volume 391, 37th International Conference on Concurrency Theory (CONCUR 2026)

Abstract
We propose a fully automated method for verifying functional correctness of message-passing concurrent programs by reducing verification problems to constrained Horn clause (CHC) solving. Inspired by RustHorn’s prophecy-based technique, we represent each sender channel by a list of values to be sent over the channel in the future, which enables modular encoding of sender and receiver threads in CHCs. To capture causal dependencies between different channels, we further attach timestamps to messages. We prove that the resulting reduction is sound and complete: a program is free from assertion failures if and only if the corresponding system of CHCs is satisfiable. We have also implemented a prototype verifier for Rust-like programs and experimentally confirmed the effectiveness of the approach.
Cite as

Takashi Nagatomi, Musashi Katsura, Naoki Kobayashi, Yusuke Matsushita, and Ken Sakayori. Prophecy-Based Automated Verification of Message-Passing Programs. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 43:1-43:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{nagatomi_et_al:LIPIcs.CONCUR.2026.43,
  author =	{Nagatomi, Takashi and Katsura, Musashi and Kobayashi, Naoki and Matsushita, Yusuke and Sakayori, Ken},
  title =	{{Prophecy-Based Automated Verification of Message-Passing Programs}},
  booktitle =	{37th International Conference on Concurrency Theory (CONCUR 2026)},
  pages =	{43:1--43:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-447-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{391},
  editor =	{Sokolova, Ana and Totzke, Patrick},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.43},
  URN =		{urn:nbn:de:0030-drops-273747},
  doi =		{10.4230/LIPIcs.CONCUR.2026.43},
  annote =	{Keywords: Program verification, message-passing concurrent programs, constrained Horn clauses, prophecies}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2026.45
Concurrent Visibility: Higher-Order Concurrency with First-Order Store

Authors: Iwan Quémerais, Guilhème Jaber, Ken Sakayori, and Davide Sangiorgi

Published in: LIPIcs, Volume 391, 37th International Conference on Concurrency Theory (CONCUR 2026)

Abstract
We propose an Operational Game Semantics for a (call-by-value) concurrent higher-order language with first-order store (references may contain other references or first-order values such as integers or booleans; however they may not store higher-order values such as functions). We adapt the game-semantic notion of visibility, which semantically captures the absence of higher-order references and developed for sequential higher-order languages, to a concurrent setting. We thus define a complete-trace preorder, and prove it sound for the contextual preorder, by introducing a synchronization-based composition of semantic configurations and establishing an observational adequacy result. We also prove completeness for the subset of the language in which functions return first-order values. In contrast to the case of sequential visibility, in the labeled transition semantics we have to account for the presence of multiple active threads with possibly different visibilities, and of a tree-like structure for managing the dependencies among the threads so created. Moreover, we have to reason on families of traces, rather than single traces, as in concurrent setting the order among certain actions cannot be enforced.
Cite as

Iwan Quémerais, Guilhème Jaber, Ken Sakayori, and Davide Sangiorgi. Concurrent Visibility: Higher-Order Concurrency with First-Order Store. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 45:1-45:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{quemerais_et_al:LIPIcs.CONCUR.2026.45,
  author =	{Qu\'{e}merais, Iwan and Jaber, Guilh\`{e}me and Sakayori, Ken and Sangiorgi, Davide},
  title =	{{Concurrent Visibility: Higher-Order Concurrency with First-Order Store}},
  booktitle =	{37th International Conference on Concurrency Theory (CONCUR 2026)},
  pages =	{45:1--45:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-447-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{391},
  editor =	{Sokolova, Ana and Totzke, Patrick},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.45},
  URN =		{urn:nbn:de:0030-drops-273760},
  doi =		{10.4230/LIPIcs.CONCUR.2026.45},
  annote =	{Keywords: Operational game semantics, higher-order effectful programs, mutable store}
}
Document
DOI: 10.4230/LIPIcs.LICS.2026.79
Wiring the π-Calculus to Denotational Semantics

Authors: Ken Sakayori, Davide Sangiorgi, Simon Castellan, and Pierre Clairambault

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract
We introduce a dialect of the Asynchronous π-calculus, called AWπ, in which (1) an input name may be owned, at any time, by at most one process; (2) each name has either only the input or only the output capability. As a result, special processes called wires (aka forwarders, that is, processes that receive values at one name and re-transmit) behave as substitutions when composed with any AWπ process. Thus AWπ naturally yields a category, whose morphisms are AWπ processes (modulo the reference behavioural equivalence, barbed congruence) and whose objects are types; and where wires act as identity morphisms. We show that the category of processes can be further organised into (sub)categories with the structures needed for the interpretation of common higher-order language features in the literature by drawing on insights from game semantics; notably, we construct a relative Seely category, the categorical structure that concurrent game semantics has. At the same time, AWπ follows the tradition of ordinary π-calculi in that expressiveness is preserved and the operational and algebraic theory are developed in a similar manner, notwithstanding substantial technical differences in their development and proofs. In short, the goal of AWπ is to remain faithful to the operational and algebraic tradition of the π-calculi while connecting to the tradition of denotational models for programming languages.
Cite as

Ken Sakayori, Davide Sangiorgi, Simon Castellan, and Pierre Clairambault. Wiring the π-Calculus to Denotational Semantics. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 79:1-79:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{sakayori_et_al:LIPIcs.LICS.2026.79,
  author =	{Sakayori, Ken and Sangiorgi, Davide and Castellan, Simon and Clairambault, Pierre},
  title =	{{Wiring the \pi-Calculus to Denotational Semantics}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{79:1--79:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.79},
  URN =		{urn:nbn:de:0030-drops-268669},
  doi =		{10.4230/LIPIcs.LICS.2026.79},
  annote =	{Keywords: \pi-calculus, denotational semantics, game semantics, wire process}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.32
Output Without Delay: A π-Calculus Compatible with Categorical Semantics

Authors: Ken Sakayori and Takeshi Tsukada

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
The quest for logical or categorical foundations of the π-calculus (not limited to session-typed variants) remains an important challenge. A categorical type theory correspondence for a variant of the i/o-typed π-calculus was recently revealed by Sakayori and Tsukada, but, at the same time, they exposed that this categorical semantics contradicts with most of the behavioural equivalences. This paper diagnoses the nature of this problem and attempts to fill the gap between categorical and operational semantics. We first identify the source of the problem to be the mismatch between the operational and categorical interpretation of a process called the forwarder. From the operational viewpoint, a forwarder may add an arbitrary delay when forwarding a message, whereas, from the categorical viewpoint, a forwarder must not add any delay when forwarding a message. Led by this observation, we introduce a calculus that can express forwarders that do not introduce delay. More specifically, the calculus we introduce is a variant of the π-calculus with a new operational semantics in which output actions are forced to happen as soon as they get unguarded. We show that this calculus (i) is compatible with the categorical semantics and (ii) can encode the standard π-calculus.
Cite as

Ken Sakayori and Takeshi Tsukada. Output Without Delay: A π-Calculus Compatible with Categorical Semantics. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 32:1-32:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{sakayori_et_al:LIPIcs.FSCD.2021.32,
  author =	{Sakayori, Ken and Tsukada, Takeshi},
  title =	{{Output Without Delay: A \pi-Calculus Compatible with Categorical Semantics}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{32:1--32:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.32},
  URN =		{urn:nbn:de:0030-drops-142705},
  doi =		{10.4230/LIPIcs.FSCD.2021.32},
  annote =	{Keywords: \pi-calculus, categorical semantics, linear approximation}
}

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact