Streamlining progress-based derivations of concurrent programs

Dongol, Brijesh and Mooij, Arjan J. (2008) Streamlining progress-based derivations of concurrent programs. Formal Aspects of Computing, 20 2: 141-160. doi:10.1007/s00165-007-0037-4

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads

Author Dongol, Brijesh
Mooij, Arjan J.
Title Streamlining progress-based derivations of concurrent programs
Journal name Formal Aspects of Computing   Check publisher's open access policy
ISSN 0934-5043
Publication date 2008-03-01
Year available 2007
Sub-type Article (original research)
DOI 10.1007/s00165-007-0037-4
Open Access Status Not Open Access
Volume 20
Issue 2
Start page 141
End page 160
Total pages 20
Editor J. M. Wing
C. B. Jones
Place of publication London, UK
Publisher Springer
Language eng
Subject 280403 Logics and Meanings of Programs
280402 Mathematical Logic and Formal Languages
780199 Other
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.
Keyword Concurrent programs
Mathematical techniques
Program derivation
Q-Index Code C1
Q-Index Status Confirmed Code
Institutional Status UQ
Additional Notes Published online: 5 June 2007

Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 4 times in Thomson Reuters Web of Science Article | Citations
Scopus Citation Count Cited 6 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Fri, 18 Apr 2008, 19:46:35 EST by Donna Clark on behalf of School of Information Technol and Elec Engineering