Modular Verification of Liveness Properties of the I/O Behavior of Imperative Programs

Abstract

One way of verifying systems whose components interact by exchanging messages, such as distributed systems or certain types of concurrent systems, is by defining a protocol that governs the communication between the components and then verifying that each component’s input and output (I/O) actions comply with its role in the protocol. In this paper, we propose a separation logic-based approach for specifying and verifying liveness properties of the I/O behavior of such components implemented as imperative programs, such as the property that a server eventually responds to each request. Our approach builds on earlier work for specifying safety properties of the I/O behavior of programs in separation logic by means of abstract nested Hoare triples, and encodes a liveness property verification problem into a termination verification problem by specifying that some appropriately chosen I/O operation (for example, the response to the N’th request, for some unknown but fixed N) will cause the program to terminate.