×

zbMATH — the first resource for mathematics

Towards automatic stability analysis for rely-guarantee proofs. (English) Zbl 1206.68084
Jones, Neil D. (ed.) et al., Verification, model checking, and abstract interpretation. 10th international conference, VMCAI 2009, Savannah, GA, USA, January 18–20, 2009. Proceedings. Berlin: Springer (ISBN 978-3-540-93899-6/pbk). Lecture Notes in Computer Science 5403, 14-28 (2009).
Summary: The Rely-Guarantee approach is a well-known compositional method for proving Hoare logic properties of concurrent programs. In this approach, predicates in the proof must be proved invariant (or stable) under interference from the environment. We describe a framework, and a prototype implementation, for automatically detecting and repairing instability in such proofs. The method uses a combination of model checking, abstract interpretation, SMT and flow-control refinement.
For the entire collection see [Zbl 1155.68009].

MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
Apron; BLAST; cvc3; Interproc
PDF BibTeX XML Cite
Full Text: DOI