Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/inria-00202930
Contributor : Clément Hurlin <>
Submitted on : Tuesday, January 8, 2008 - 2:22:26 PM
Last modification on : Saturday, January 27, 2018 - 1:30:49 AM
Long-term archiving on: : Tuesday, April 13, 2010 - 4:42:21 PM

Files

vamp07.pdf
Files produced by the author(s)

Identifiers

  • 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. ⟨inria-00202930⟩

Share

Metrics

Record views

188

Files downloads

217