System-level state equality detection for the formal dynamic verification of legacy distributed applications

Marion Guthmuller 1 Gabriel Corona 1 Martin Quinson 2
1 LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
2 MYRIADS - Design and Implementation of Autonomous Distributed Systems
Inria Rennes – Bretagne Atlantique , IRISA-D1 - SYSTÈMES LARGE ÉCHELLE
Abstract : The ever increasing complexity of distributed systems mandates to formally verify their design and implementation. Unfortunately, the common approaches and existing tools to formally establish the correctness of these systems remain hardly applicable to most legacy HPC applications, that are commonly written in Fortran or C/C++, using the MPI standard. This work addresses the problem of automatically detecting at system-level the equality of the application's state. This allows to automatically verify safety and liveness properties on legacy HPC applications. We present how this state equality detection can be achieved without any source code static analysis, but at runtime using memory introspection and classical debugging techniques. We demonstrate the effectiveness of our approach through the exhaustive verification of several programs from the MPICH3 test suite and through the partial termination analysis of some applications from the Competition on Software Verification (SV-COMP).
Document type :
Journal articles
Complete list of metadatas

Cited literature [32 references]  Display  Hide  Download
https://hal.inria.fr/hal-01900120
Contributor : Martin Quinson <>
Submitted on : Saturday, October 20, 2018 - 10:38:36 PM
Last modification on : Friday, September 13, 2019 - 9:51:33 AM

File

journal.pdf
Files produced by the author(s)

Identifiers

Collections

CNRS | UNIV-RENNES1 | UNIV-LORRAINE | LORIA | CENTRALESUPELEC | IRISA | INRIA | UNIV-RENNES | UR1-UFR-ISTIC | GRID5000 | ENS-RENNES

Citation

Marion Guthmuller, Gabriel Corona, Martin Quinson. System-level state equality detection for the formal dynamic verification of legacy distributed applications. Journal of Logical and Algebraic Methods in Programming, Elsevier, 2018, 96, pp.1 - 11. ⟨10.1016/j.jlamp.2017.12.004⟩. ⟨hal-01900120⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

105

Files downloads

150

Contact


archive-ouverte@inria.fr