The stability problem for verification of concurrent object-oriented programs - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2007

The stability problem for verification of concurrent object-oriented programs

Résumé

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
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

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

Identifiants

  • HAL Id : inria-00202930 , version 1

Citer

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⟩

Collections

INRIA INRIA2
96 Consultations
125 Téléchargements

Partager

Gmail Facebook X LinkedIn More