# Bilateral Proofs of Safety and Progress Properties of Concurrent Programs

## TL;DR

This paper introduces a bilateral compositional proof system for verifying safety and progress properties of concurrent programs, enabling modular verification and specification composition even with unavailable source code.

## Contribution

It develops a novel bilateral proof technique and composition rules for concurrent program specifications, facilitating modular verification and integration.

## Key findings

- Proof techniques for verification of concurrent programs
- Composition rules for deriving program specifications
- Applicable to cross-vendor program integration

## Abstract

This paper suggests a theomisra@utexas.edury of composable specification of concurrent programs that permits: (1) verification of program code for a given specification, and (2) composition of the specifications of the components to yield the specification of a program. The specification consists of both terminal properties that hold at the end of a program execution (if the execution terminates) and perpetual properties that hold throughout an execution. We devise (1) proof techniques for verification, and (2) composition rules to derive the specification of a program from those of its components. We employ terminal properties of components to derive perpetual properties of a program and conversely. Hence, this proof strategy is called bilateral. The compositional aspect of the theory is important in assembling a program out of components some of whose source code may not be available, as is increasingly the case with cross-vendor program integration.