Event Details
Concurrency Verification: Why? And How?
Presenter: Willem-Paul de Roever - University of Kiel, Germany
Supervisor:
Date: Mon, March 18, 2002
Time: 15:30:00 - 00:00:00
Place: EOW 430
ABSTRACT
Abstract:
The relevance of correctness proofs for concurrent programs will be argued by answering the following questions:
- How important is verification for the development of correct software?
- Why does one need to give correctness proofs for concurrent programs? Must these be formal? Or even machine-checked?
- Which style of proof method is more appropriate, a compositional or noncompositional one?
No standard answer can be given to the third question. For, when verifying a large program compositionally, it reduces its verification first to the independent verification of its parts, and then proves that the specifications satisfied by these parts imply the desired property of the original large program. However, for this strategy to work, first an appropriate decomposition of that large program should be found.
Literature: Concurrency Verification: Introduction to Compositional and Noncompositional Methods, by W.-P. de Roever, F.S. de Boer, et al., Cambridge Tracts in Theoretical Computer Science 54, Cambridge University Press, 2001.