The stability problem for verification of concurrent object-oriented programs - Archive ouverte HAL Access content directly
Conference Papers Year : 2007

The stability problem for verification of concurrent object-oriented programs

(1) , (1)


Modular static verification of concurrent object-oriented programs remains a challenge. This paper discusses the impact of concurrency on the use and meaning of behavioural specifications, and in particular on method contracts and class invariants. Atomicity of methods is often advocated as a solution to the problem of verification of multithreaded programs. However, in a design-by-contract framework atomicity in itself is not sufficient, because it does not consider specifications. Instead, we propose to use the notion of stability of method contracts to allow sound modular reasoning about method calls. A contract is stable if it cannot be broken by interferences from concurrent threads. We explain why stability of contracts cannot always be shown directly, and we speculate about different approaches to prove stability. Finally, we outline how a proof obligation generator for sequential programs can be extended to one for concurrent programs by using stability information. This paper does not present a full technical solution to the problem, but instead shows how it can be decomposed into several smaller subproblems. For each subproblem, a solution is sketched, but the technical details still need to be worked out.
Fichier principal
Vignette du fichier
vamp07.pdf (203.95 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

inria-00202930 , version 1 (08-01-2008)


  • HAL Id : inria-00202930 , version 1


Marieke Huisman, Clément Hurlin. The stability problem for verification of concurrent object-oriented programs. Verification and Analysis of Multi-threaded Java-like Programs, Sep 2007, Lisbonne, Portugal. pp.52. ⟨inria-00202930⟩


94 View
120 Download


Gmail Facebook Twitter LinkedIn More