2026-08-07T07:37:44Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16742 2024-03-06T10:58:12Z ddc:004 open_access

Compositional Verification of Interacting Systems Using Event Monads Zhan, Bohua Lv, Yi Wang, Shuling Zhao, Gehang Hao, Jifeng Ye, Hong Xia, Bican Hoare Logic Compositional Verification Events Large software systems are usually divided into multiple components that interact with each other. How to verify interacting components in a modular way is one of the major problems in formal verification. In many cases, interaction between components can be modeled asynchronously, where events are sent without requiring a response in order to continue with execution of the component. In this paper, we propose a lightweight, event-based framework for verification of components with asynchronous interaction. We define event monads and event systems, and a Hoare logic-style calculus for reasoning about them. The framework is implemented in Isabelle and applied to several case studies, including models for distributed computing, cache-coherence protocols, and verification of partition scheduling in a real-time operating system. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Bohua Zhan and Yi Lv and Shuling Wang and Gehang Zhao and Jifeng Hao and Hong Ye and Bican Xia 2022 Is Part Of LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2022.33 urn:nbn:de:0030-drops-167420 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.33 eng https://creativecommons.org/licenses/by/4.0/legalcode