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 for this software
References in zbMATH (referenced in 7 articles , 1 standard article )
Showing results 1 to 7 of 7.
- Thomsen, Bent; Luckow, Kasper Søe; Leth, Lone; Bøgholm, Thomas: From safety critical Java programs to timed process models (2015)
- Huisman, Marieke; Gurov, Dilian: CVPP: a tool set for compositional verification of control-flow safety properties (2011)
- Soleimanifard, Siavash; Gurov, Dilian; Huisman, Marieke: ProMoVer: Modular verification of temporal safety properties (2011)
- Khot, Subhash: Inapproximability results for computational problems on lattices (2010)
- Islam, Md.Rafiqul: Mathematical modeling of age specific marital fertility rates in urban area of Bangladesh (2005)
- Feige, Uriel; Micciancio, Daniele: The inapproximability of lattice and coding problems with preprocessing (2004)
- Islam, Md.Rafiqul; Ali, M.Korban: Mathematical modeling of age specific fertility rates and study the reproductivity in the rural area of Bangladesh during 1980-1998 (2004)