| ||||
| ||||
![]() Title:Compositional Verification of Interacting Systems Using Event Monads Conference:ITP 2022 Tags:Compositional Verification, Events and Hoare Logic Abstract: 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 calculi 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. Compositional Verification of Interacting Systems Using Event Monads ![]() Compositional Verification of Interacting Systems Using Event Monads | ||||
Copyright © 2002 – 2025 EasyChair |