Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
CVPP: A Tool Set for Compositional Verification of Control-Flow Safety Properties
Univ Twente, Enschede, Netherlands.
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-0074-8786
2011 (English)In: FORMAL VERIFICATION OF OBLECT-ORIENTED SOFTWARE / [ed] Beckert, B; Marche, C, 2011, Vol. 6528, 107-121 p.Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
2011. Vol. 6528, 107-121 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 6528
Keyword [en]
PROGRAMS, CHECKING
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:kth:diva-50734ISI: 000296413000008Scopus ID: 2-s2.0-79551608474OAI: oai:DiVA.org:kth-50734DiVA: diva2:462639
Conference
International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), Paris, FRANCE, JUN 28-30, 2010
Note

QC 20111208

Available from: 2011-12-07 Created: 2011-12-07 Last updated: 2017-06-09Bibliographically approved

Open Access in DiVA

No full text

Scopus

Authority records BETA

Gurov, Dilian

Search in DiVA

By author/editor
Gurov, Dilian
By organisation
Theoretical Computer Science, TCS
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

urn-nbn
Total: 27 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf