Streamlining progress-based derivations of concurrent programs

B. Dongol, A.J. Mooij

Research output: Contribution to journalArticleAcademicpeer-review

6 Citations (Scopus)

Abstract

The logic of Owicki and Gries is a well-known logic for verifying safety properties of concurrent programs. Using this logic, Feijen and van Gasteren describe a method for deriving concurrent programs based on safety. In this work, we explore derivation techniques of concurrent programs using progress-based reasoning. We use a framework that combines the safety logic of Owicki and Gries, and the progress logic of UNITY. Our contributions improve the applicability of our earlier techniques by reducing the calculational overhead in the formal proofs and derivations. To demonstrate the effectiveness of our techniques, a derivation of Dekker’s mutual exclusion algorithm is presented. This derivation leads to the discovery of some new and simpler variants of this famous algorithm.
Original languageEnglish
Pages (from-to)141-160
JournalFormal Aspects of Computing
Volume20
Issue number2
DOIs
Publication statusPublished - 2008

Fingerprint Dive into the research topics of 'Streamlining progress-based derivations of concurrent programs'. Together they form a unique fingerprint.

Cite this