CVPP: A Tool Set for Compositonal Verification of Control-Flow Safety Properties.

Marieke Huisman, Dilian Gurov

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

8 Downloads (Pure)

Abstract

This paper describes CVPP, a tool set for compositional verification of control–flow safety properties for programs with procedures. The compositional verification principle that underlies CVPP is based on maximal models constructed from component specifications. Maximal models replace the actual components when verifying the whole program, either for the purposes of modularity of verification or due to unavailability of the component implementations at verification time. A characteristic feature of the principle and the tool set is the distinction between program structure and behaviour. While behavioural properties are more abstract and convenient for specification purposes, structural ones are easier to manipulate, in particular when it comes to verification or the construction of maximal models. Therefore, CVPP also contains the means to characterise a given behavioural formula by a set of structural formulae. The paper presents the underlying framework for compositional verification and the components of the tool set. Several verification scenarios are described, as well as wrapper tools that support the automatic execution of such scenarios, providing appropriate pre– and post–processing to interface smoothly with the user and to encapsulate the inner workings of the tool set.
Original languageUndefined
Title of host publicationFormal Verification of Object-Oriented Software (FoVeOOS) 2010.
EditorsBernhard Beckert, Claude Marche
Place of PublicationBerlin
PublisherSpringer
Pages107-121
Number of pages15
ISBN (Print)978-3-642-18070-5
DOIs
Publication statusPublished - 2010

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume6528

Keywords

  • IR-72646
  • EWI-18325
  • METIS-270993

Cite this

Huisman, M., & Gurov, D. (2010). CVPP: A Tool Set for Compositonal Verification of Control-Flow Safety Properties. In B. Beckert, & C. Marche (Eds.), Formal Verification of Object-Oriented Software (FoVeOOS) 2010. (pp. 107-121). (Lecture Notes in Computer Science; Vol. 6528). Berlin: Springer. https://doi.org/10.1007/978-3-642-18070-5_8
Huisman, Marieke ; Gurov, Dilian. / CVPP: A Tool Set for Compositonal Verification of Control-Flow Safety Properties. Formal Verification of Object-Oriented Software (FoVeOOS) 2010.. editor / Bernhard Beckert ; Claude Marche. Berlin : Springer, 2010. pp. 107-121 (Lecture Notes in Computer Science).
@inproceedings{a547c11ece1549f1bdc47de909ee81e3,
title = "CVPP: A Tool Set for Compositonal Verification of Control-Flow Safety Properties.",
abstract = "This paper describes CVPP, a tool set for compositional verification of control–flow safety properties for programs with procedures. The compositional verification principle that underlies CVPP is based on maximal models constructed from component specifications. Maximal models replace the actual components when verifying the whole program, either for the purposes of modularity of verification or due to unavailability of the component implementations at verification time. A characteristic feature of the principle and the tool set is the distinction between program structure and behaviour. While behavioural properties are more abstract and convenient for specification purposes, structural ones are easier to manipulate, in particular when it comes to verification or the construction of maximal models. Therefore, CVPP also contains the means to characterise a given behavioural formula by a set of structural formulae. The paper presents the underlying framework for compositional verification and the components of the tool set. Several verification scenarios are described, as well as wrapper tools that support the automatic execution of such scenarios, providing appropriate pre– and post–processing to interface smoothly with the user and to encapsulate the inner workings of the tool set.",
keywords = "IR-72646, EWI-18325, METIS-270993",
author = "Marieke Huisman and Dilian Gurov",
year = "2010",
doi = "10.1007/978-3-642-18070-5_8",
language = "Undefined",
isbn = "978-3-642-18070-5",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "107--121",
editor = "Bernhard Beckert and Claude Marche",
booktitle = "Formal Verification of Object-Oriented Software (FoVeOOS) 2010.",

}

Huisman, M & Gurov, D 2010, CVPP: A Tool Set for Compositonal Verification of Control-Flow Safety Properties. in B Beckert & C Marche (eds), Formal Verification of Object-Oriented Software (FoVeOOS) 2010.. Lecture Notes in Computer Science, vol. 6528, Springer, Berlin, pp. 107-121. https://doi.org/10.1007/978-3-642-18070-5_8

CVPP: A Tool Set for Compositonal Verification of Control-Flow Safety Properties. / Huisman, Marieke; Gurov, Dilian.

Formal Verification of Object-Oriented Software (FoVeOOS) 2010.. ed. / Bernhard Beckert; Claude Marche. Berlin : Springer, 2010. p. 107-121 (Lecture Notes in Computer Science; Vol. 6528).

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

TY - GEN

T1 - CVPP: A Tool Set for Compositonal Verification of Control-Flow Safety Properties.

AU - Huisman, Marieke

AU - Gurov, Dilian

PY - 2010

Y1 - 2010

N2 - This paper describes CVPP, a tool set for compositional verification of control–flow safety properties for programs with procedures. The compositional verification principle that underlies CVPP is based on maximal models constructed from component specifications. Maximal models replace the actual components when verifying the whole program, either for the purposes of modularity of verification or due to unavailability of the component implementations at verification time. A characteristic feature of the principle and the tool set is the distinction between program structure and behaviour. While behavioural properties are more abstract and convenient for specification purposes, structural ones are easier to manipulate, in particular when it comes to verification or the construction of maximal models. Therefore, CVPP also contains the means to characterise a given behavioural formula by a set of structural formulae. The paper presents the underlying framework for compositional verification and the components of the tool set. Several verification scenarios are described, as well as wrapper tools that support the automatic execution of such scenarios, providing appropriate pre– and post–processing to interface smoothly with the user and to encapsulate the inner workings of the tool set.

AB - This paper describes CVPP, a tool set for compositional verification of control–flow safety properties for programs with procedures. The compositional verification principle that underlies CVPP is based on maximal models constructed from component specifications. Maximal models replace the actual components when verifying the whole program, either for the purposes of modularity of verification or due to unavailability of the component implementations at verification time. A characteristic feature of the principle and the tool set is the distinction between program structure and behaviour. While behavioural properties are more abstract and convenient for specification purposes, structural ones are easier to manipulate, in particular when it comes to verification or the construction of maximal models. Therefore, CVPP also contains the means to characterise a given behavioural formula by a set of structural formulae. The paper presents the underlying framework for compositional verification and the components of the tool set. Several verification scenarios are described, as well as wrapper tools that support the automatic execution of such scenarios, providing appropriate pre– and post–processing to interface smoothly with the user and to encapsulate the inner workings of the tool set.

KW - IR-72646

KW - EWI-18325

KW - METIS-270993

U2 - 10.1007/978-3-642-18070-5_8

DO - 10.1007/978-3-642-18070-5_8

M3 - Conference contribution

SN - 978-3-642-18070-5

T3 - Lecture Notes in Computer Science

SP - 107

EP - 121

BT - Formal Verification of Object-Oriented Software (FoVeOOS) 2010.

A2 - Beckert, Bernhard

A2 - Marche, Claude

PB - Springer

CY - Berlin

ER -

Huisman M, Gurov D. CVPP: A Tool Set for Compositonal Verification of Control-Flow Safety Properties. In Beckert B, Marche C, editors, Formal Verification of Object-Oriented Software (FoVeOOS) 2010.. Berlin: Springer. 2010. p. 107-121. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-18070-5_8