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:

  1. How important is verification for the development of correct software?
  2. Why does one need to give correctness proofs for concurrent programs? Must these be formal? Or even machine-checked?
  3. Which style of proof method is more appropriate, a compositional or noncompositional one?
The answers to the first question is given by considering a problem which is characteristic for the area, and for which we consider a number of increasingly complicated incorrect approximations until we finally arrive at an allegedly correct solution. The question whether verification should be machine-checked or not depends on the amount of money involved in correcting bugs, which can run into many millions of dollars.

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.