Document Open Access Logo

Prophecy-Based Automated Verification of Message-Passing Programs

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

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2026.43.pdf
  • Filesize: 0.87 MB
  • 21 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Program verification
  • message-passing concurrent programs
  • constrained Horn clauses
  • prophecies

Metrics

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.CONCUR.2026.43

Author Details

Takashi Nagatomi
  • The University of Tokyo, Japan
Musashi Katsura
  • The University of Tokyo, Japan
Naoki Kobayashi
  • The University of Tokyo, Japan
Yusuke Matsushita
  • Kyoto University, Japan
  • MPI-SWS, Kaiserslautern, Germany
Ken Sakayori
  • The University of Tokyo, Japan

Funding

  • Kobayashi, Naoki: JSPS KAKENHI Grant Numbers JP20H05703, JP26H02486.
  • Matsushita, Yusuke: Hakubi Project at Kyoto University, JSPS KAKENHI Grant Number JP24KJ0133.
  • Sakayori, Ken: JSPS KAKENHI Grant Numbers JP24K20731, JP26H02486.

References

  1. Martín Abadi and Leslie Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253-284, 1991. URL: https://doi.org/10.1016/0304-3975(91)90224-P.
  2. Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. In Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS '93), Montreal, Canada, June 19-23, 1993, pages 160-170. IEEE Computer Society, 1993. URL: https://doi.org/10.1109/LICS.1993.287591.
  3. Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press, 2008. Google Scholar
  4. Romain Beauxis, Catuscia Palamidessi, and Frank D. Valencia. On the asynchronous nature of the asynchronous pi-calculus. In Pierpaolo Degano, Rocco De Nicola, and José Meseguer, editors, Concurrency, Graphs and Models, Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday, Lecture Notes in Computer Science, pages 473-492. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-68679-8_29.
  5. Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan, and Andrey Rybalchenko. Horn clause solvers for program verification. In Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, volume 9300 of LNCS, pages 24-51. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-23534-9_2.
  6. Toby Cathcart Burn, C.-H. Luke Ong, and Steven J. Ramsay. Higher-order constrained Horn clauses for verification. Proc. ACM Program. Lang., 2(POPL):11:1-11:28, 2018. URL: https://doi.org/10.1145/3158099.
  7. Adrien Champion, Naoki Kobayashi, and Ryosuke Sato. HoIce: An ICE-based non-linear Horn clause solver. In Sukyoung Ryu, editor, Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings, volume 11275 of Lecture Notes in Computer Science, pages 146-156. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-02768-1_8.
  8. Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. The MIT Press, 1999. Google Scholar
  9. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors. Handbook of Model Checking. Springer, 2018. Google Scholar
  10. Emanuele De Angelis, Fabio Fioravanti, John P. Gallagher, Manuel V. Hermenegildo, Alberto Pettorossi, and Maurizio Proietti. Analysis and transformation of constrained Horn clauses for program verification. Theory and Practice of Logic Programming, 22(6):974-1042, 2022. URL: https://doi.org/10.1017/S1471068421000211.
  11. Xavier Denis, Jacques-Henri Jourdan, and Claude Marché. Creusot: A foundry for the deductive verification of Rust programs. In International Conference on Formal Engineering Methods, pages 90-105. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-17244-1_6.
  12. Cormac Flanagan, Stephen N. Freund, and Shaz Qadeer. Thread-modular verification for shared-memory programs. In Daniel Le Métayer, editor, Programming Languages and Systems, 11th European Symposium on Programming, ESOP 2002, held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings, Lecture Notes in Computer Science, pages 262-277. Springer, 2002. URL: https://doi.org/10.1007/3-540-45927-8_19.
  13. Travis Hance, Laila Elbeheiry, Yusuke Matsushita, and Derek Dreyer. VerusBelt: A semantic foundation for Verus’s proof-oriented extensions to the Rust type system. Proc. ACM Program. Lang., 10(PLDI), June 2026. URL: https://doi.org/10.1145/3808325.
  14. Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Shaz Qadeer. Thread-modular abstraction refinement. In Warren A. Hunt Jr. and Fabio Somenzi, editors, Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings, Lecture Notes in Computer Science, pages 262-274. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45069-6_27.
  15. Hossein Hojjat and Philipp Rümmer. The ELDARICA Horn solver. In 2018 Formal Methods in Computer Aided Design (FMCAD), pages 1-7. IEEE, 2018. URL: https://doi.org/10.23919/FMCAD.2018.8603013.
  16. Hans Hüttel, Ivan Lanese, Vasco T Vasconcelos, Luís Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, et al. Foundations of session types and behavioural contracts. ACM Computing Surveys (CSUR), 49(1):1-36, 2016. URL: https://doi.org/10.1145/2873052.
  17. Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs. The future is ours: prophecy variables in separation logic. Proceedings of the ACM on Programming Languages, 4(POPL):1-32, 2019. URL: https://doi.org/10.1145/3371113.
  18. Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In Sriram K. Rajamani and David Walker, editors, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 637-650. ACM, 2015. URL: https://doi.org/10.1145/2676726.2676980.
  19. Hiroyuki Katsura, Naoki Kobayashi, Ken Sakayori, and Ryosuke Sato. Automated catamorphism synthesis for solving constrained Horn clauses over algebraic data types. In International Static Analysis Symposium, pages 305-327. Springer, 2025. URL: https://doi.org/10.1007/978-3-032-07106-4_13.
  20. Naoki Kobayashi. Type systems for concurrent programs. In Formal Methods at the Crossroads. From Panacea to Foundational Support: 10th Anniversary Colloquium of UNU/IIST, the International Institute for Software Technology of The United Nations University, Lisbon, Portugal, March 18-20, 2002. Revised Papers, pages 439-453. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-40007-3_26.
  21. Naoki Kobayashi, Takeshi Nishikawa, Atsushi Igarashi, and Hiroshi Unno. Temporal verification of programs via first-order fixpoint logic. In Bor-Yuh Evan Chang, editor, Static Analysis - 26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, Proceedings, volume 11822 of Lecture Notes in Computer Science, pages 413-436. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-32304-2_20.
  22. Naoki Kobayashi, Ryosuke Sato, Ayumi Shinohara, and Ryo Yoshinaka. Solvable tuple patterns and their applications to program verification. Proc. ACM Program. Lang., 10(PLDI), June 2026. URL: https://doi.org/10.1145/3808258.
  23. Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, and Takeshi Tsukada. HFL(Z) validity checking for automated program verification. Proc. ACM Program. Lang., 7(POPL):154-184, 2023. URL: https://doi.org/10.1145/3571199.
  24. Naoki Kobayashi, Takeshi Tsukada, and Keiichi Watanabe. Higher-order program verification via HFL model checking. In Amal Ahmed, editor, Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Lecture Notes in Computer Science, pages 711-738. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89884-1_25.
  25. Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. SMT-based model checking for recursive programs. Formal Methods Syst. Des., 48(3):175-205, 2016. URL: https://doi.org/10.1007/s10703-016-0249-4.
  26. Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. Verus: Verifying Rust programs using linear ghost types. Proc. ACM Program. Lang., 7(OOPSLA1):286-315, 2023. URL: https://doi.org/10.1145/3586037.
  27. Alexander Malkis, Andreas Podelski, and Andrey Rybalchenko. Precise thread-modular verification. In Hanne Riis Nielson and Gilberto Filé, editors, Static Analysis, pages 218-232, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-74061-2_14.
  28. Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, and Derek Dreyer. RustHornBelt: A semantic foundation for functional verification of Rust programs with unsafe code. In Ranjit Jhala and Isil Dillig, editors, PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022, pages 841-856. ACM, 2022. URL: https://doi.org/10.1145/3519939.3523704.
  29. Yusuke Matsushita and Takeshi Tsukada. Nola: Later-free ghost state for verifying termination in Iris. Proc. ACM Program. Lang., 9(PLDI):98-124, 2025. URL: https://doi.org/10.1145/3729250.
  30. Yusuke Matsushita, Takeshi Tsukada, and Naoki Kobayashi. RustHorn: CHC-based verification for Rust programs. ACM Transactions on Programming Languages and Systems (TOPLAS), 43(4):1-54, 2021. URL: https://doi.org/10.1145/3462205.
  31. Takashi Nagatomi, Musashi Katsura, Naoki Kobayashi, Yusuke Matsushita, and Ken Sakayori. Prophecy-based automated verification of message-passing programs (full version). CoRR, 2026. URL: https://doi.org/10.48550/arXiv.2606.28066.
  32. Hiromi Ogawa, Taro Sekiyama, and Hiroshi Unno. Thrust: A prophecy-based refinement type system for Rust. Proc. ACM Program. Lang., 9(PLDI):2056-2080, 2025. URL: https://doi.org/10.1145/3729333.
  33. Toby Ueno and Ankush Das. Practical refinement session type inference. In Robbert Krebbers, editor, Programming Languages and Systems, pages 298-330, Cham, 2026. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-032-22723-2_11.
  34. Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen. Modular primal-dual fixpoint logic solving for temporal verification. Proc. ACM Program. Lang., 7(POPL):2111-2140, 2023. URL: https://doi.org/10.1145/3571265.
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