The stability problem for verification of concurrent object-oriented programs

Marieke Huisman 1 Clément Hurlin 1
1 EVEREST - Environments for Verification and Security of Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : 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.
Type de document :
Communication dans un congrès
Verification and Analysis of Multi-threaded Java-like Programs, Sep 2007, Lisbonne, Portugal. pp.52, 2007
Liste complète des métadonnées

https://hal.inria.fr/inria-00202930
Contributeur : Clément Hurlin <>
Soumis le : mardi 8 janvier 2008 - 14:22:26
Dernière modification le : samedi 27 janvier 2018 - 01:30:49
Document(s) archivé(s) le : mardi 13 avril 2010 - 16:42:21

Fichiers

vamp07.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00202930, version 1

Collections

Citation

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, 2007. 〈inria-00202930〉

Partager

Métriques

Consultations de la notice

156

Téléchargements de fichiers

185