ProMoVer: Modular Verification of Temporal Safety Properties.

Siavash Soleimanifard, Dilian Gurov, Marieke Huisman

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

4 Citations (Scopus)

Abstract

This paper describes ProMoVer, a tool for fully automated procedure–modular verification of Java programs equipped with method–local and global assertions that specify safety properties of sequences of method invocations. Modularity at the procedure–level is a natural instantiation of the modular verification paradigm, where correctness of global properties is relativized on the local properties of the methods rather than on their implementations, and is based here on the construction of maximal models for a program model that abstracts away from program data. This approach allows global properties to be verified in the presence of code evolution, multiple method implementations (as arising from software product lines), or even unknown method implementations (as in mobile code for open platforms). ProMoVer automates a typical verification scenario for a previously developed tool set for compositional verification of control flow safety properties, and provides appropriate pre– and post–processing. Modularity is exploited by a mechanism for proof reuse that detects and minimizes the verification tasks resulting from changes in the code and the specifications. The verification task is relatively light–weight due to support for abstraction from private methods and automatic extraction of candidate specifications from method implementations. We evaluate the tool on a number of applications from the smart card domain.
Original languageUndefined
Title of host publicationProceedings of the 9th International Conference on Software Engineering and Formal Methods (SEFM 2011)
EditorsGilles Barthe, Alberto Pardo, Gerardo Schneider
Place of PublicationBerlin
PublisherSpringer
Pages366-381
Number of pages16
ISBN (Print)978-3-642-24690-6
DOIs
Publication statusPublished - Nov 2011
Event9th International Conference on Software Engineering and Formal Methods, SEFM 2011 - Montevideo, Uruguay
Duration: 14 Nov 201118 Nov 2011
Conference number: 9

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume7041

Conference

Conference9th International Conference on Software Engineering and Formal Methods, SEFM 2011
Abbreviated titleSEFM
CountryUruguay
CityMontevideo
Period14/11/1118/11/11

Keywords

  • METIS-281578
  • EWI-20830
  • IR-78615

Cite this

Soleimanifard, S., Gurov, D., & Huisman, M. (2011). ProMoVer: Modular Verification of Temporal Safety Properties. In G. Barthe, A. Pardo, & G. Schneider (Eds.), Proceedings of the 9th International Conference on Software Engineering and Formal Methods (SEFM 2011) (pp. 366-381). (Lecture Notes in Computer Science; Vol. 7041). Berlin: Springer. https://doi.org/10.1007/978-3-642-24690-6_25
Soleimanifard, Siavash ; Gurov, Dilian ; Huisman, Marieke. / ProMoVer: Modular Verification of Temporal Safety Properties. Proceedings of the 9th International Conference on Software Engineering and Formal Methods (SEFM 2011). editor / Gilles Barthe ; Alberto Pardo ; Gerardo Schneider. Berlin : Springer, 2011. pp. 366-381 (Lecture Notes in Computer Science).
@inproceedings{adda59f7201041f8abd8b6d8dd9f5cef,
title = "ProMoVer: Modular Verification of Temporal Safety Properties.",
abstract = "This paper describes ProMoVer, a tool for fully automated procedure–modular verification of Java programs equipped with method–local and global assertions that specify safety properties of sequences of method invocations. Modularity at the procedure–level is a natural instantiation of the modular verification paradigm, where correctness of global properties is relativized on the local properties of the methods rather than on their implementations, and is based here on the construction of maximal models for a program model that abstracts away from program data. This approach allows global properties to be verified in the presence of code evolution, multiple method implementations (as arising from software product lines), or even unknown method implementations (as in mobile code for open platforms). ProMoVer automates a typical verification scenario for a previously developed tool set for compositional verification of control flow safety properties, and provides appropriate pre– and post–processing. Modularity is exploited by a mechanism for proof reuse that detects and minimizes the verification tasks resulting from changes in the code and the specifications. The verification task is relatively light–weight due to support for abstraction from private methods and automatic extraction of candidate specifications from method implementations. We evaluate the tool on a number of applications from the smart card domain.",
keywords = "METIS-281578, EWI-20830, IR-78615",
author = "Siavash Soleimanifard and Dilian Gurov and Marieke Huisman",
note = "10.1007/978-3-642-24690-6_25",
year = "2011",
month = "11",
doi = "10.1007/978-3-642-24690-6_25",
language = "Undefined",
isbn = "978-3-642-24690-6",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "366--381",
editor = "Gilles Barthe and Alberto Pardo and Gerardo Schneider",
booktitle = "Proceedings of the 9th International Conference on Software Engineering and Formal Methods (SEFM 2011)",

}

Soleimanifard, S, Gurov, D & Huisman, M 2011, ProMoVer: Modular Verification of Temporal Safety Properties. in G Barthe, A Pardo & G Schneider (eds), Proceedings of the 9th International Conference on Software Engineering and Formal Methods (SEFM 2011). Lecture Notes in Computer Science, vol. 7041, Springer, Berlin, pp. 366-381, 9th International Conference on Software Engineering and Formal Methods, SEFM 2011, Montevideo, Uruguay, 14/11/11. https://doi.org/10.1007/978-3-642-24690-6_25

ProMoVer: Modular Verification of Temporal Safety Properties. / Soleimanifard, Siavash; Gurov, Dilian; Huisman, Marieke.

Proceedings of the 9th International Conference on Software Engineering and Formal Methods (SEFM 2011). ed. / Gilles Barthe; Alberto Pardo; Gerardo Schneider. Berlin : Springer, 2011. p. 366-381 (Lecture Notes in Computer Science; Vol. 7041).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - ProMoVer: Modular Verification of Temporal Safety Properties.

AU - Soleimanifard, Siavash

AU - Gurov, Dilian

AU - Huisman, Marieke

N1 - 10.1007/978-3-642-24690-6_25

PY - 2011/11

Y1 - 2011/11

N2 - This paper describes ProMoVer, a tool for fully automated procedure–modular verification of Java programs equipped with method–local and global assertions that specify safety properties of sequences of method invocations. Modularity at the procedure–level is a natural instantiation of the modular verification paradigm, where correctness of global properties is relativized on the local properties of the methods rather than on their implementations, and is based here on the construction of maximal models for a program model that abstracts away from program data. This approach allows global properties to be verified in the presence of code evolution, multiple method implementations (as arising from software product lines), or even unknown method implementations (as in mobile code for open platforms). ProMoVer automates a typical verification scenario for a previously developed tool set for compositional verification of control flow safety properties, and provides appropriate pre– and post–processing. Modularity is exploited by a mechanism for proof reuse that detects and minimizes the verification tasks resulting from changes in the code and the specifications. The verification task is relatively light–weight due to support for abstraction from private methods and automatic extraction of candidate specifications from method implementations. We evaluate the tool on a number of applications from the smart card domain.

AB - This paper describes ProMoVer, a tool for fully automated procedure–modular verification of Java programs equipped with method–local and global assertions that specify safety properties of sequences of method invocations. Modularity at the procedure–level is a natural instantiation of the modular verification paradigm, where correctness of global properties is relativized on the local properties of the methods rather than on their implementations, and is based here on the construction of maximal models for a program model that abstracts away from program data. This approach allows global properties to be verified in the presence of code evolution, multiple method implementations (as arising from software product lines), or even unknown method implementations (as in mobile code for open platforms). ProMoVer automates a typical verification scenario for a previously developed tool set for compositional verification of control flow safety properties, and provides appropriate pre– and post–processing. Modularity is exploited by a mechanism for proof reuse that detects and minimizes the verification tasks resulting from changes in the code and the specifications. The verification task is relatively light–weight due to support for abstraction from private methods and automatic extraction of candidate specifications from method implementations. We evaluate the tool on a number of applications from the smart card domain.

KW - METIS-281578

KW - EWI-20830

KW - IR-78615

U2 - 10.1007/978-3-642-24690-6_25

DO - 10.1007/978-3-642-24690-6_25

M3 - Conference contribution

SN - 978-3-642-24690-6

T3 - Lecture Notes in Computer Science

SP - 366

EP - 381

BT - Proceedings of the 9th International Conference on Software Engineering and Formal Methods (SEFM 2011)

A2 - Barthe, Gilles

A2 - Pardo, Alberto

A2 - Schneider, Gerardo

PB - Springer

CY - Berlin

ER -

Soleimanifard S, Gurov D, Huisman M. ProMoVer: Modular Verification of Temporal Safety Properties. In Barthe G, Pardo A, Schneider G, editors, Proceedings of the 9th International Conference on Software Engineering and Formal Methods (SEFM 2011). Berlin: Springer. 2011. p. 366-381. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-24690-6_25