DROPS

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}
}

Search Results

Documents authored by Katsura, Musashi

Prophecy-Based Automated Verification of Message-Passing Programs

Abstract

Cite as

Thanks for your feedback!

Could not send message