Algorithmic verification of procedural programs in the presence of code variability
2015 (English)In: Formal Aspects of Component Software: 11th International Symposium, FACS 2014, Bertinoro, Italy, September 10-12, 2014, Revised Selected Papers, Springer, 2015, Vol. 8997, 41 p.327-345 p.Conference paper (Refereed)
We present a generic framework for verifying temporal safety properties of procedural programs that are dynamically or statically configured by replacing, adapting, or adding new components. To deal with such a variability of a program, we require programmers to provide local specifications for its variable components, and verify the global properties by replacing these specifications with maximal models. Our framework is a generalization of a previously developed framework that abstracts from all program data. In this work, we capture program data and thus significantly increase the range of properties that can be verified. Our framework is generic by being parametric on the set of observed program events and their semantics. We separate program structure from the behavior it induces to facilitate independent component specification and verification. We provide tool support for an instantiation of our framework to programs written in a procedural language with pointers as the only datatype.
Place, publisher, year, edition, pages
Springer, 2015. Vol. 8997, 41 p.327-345 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 8997
Algorithms, Computer software, Semantics, Algorithmic verification, Generic frameworks, Global properties, Independent components, New components, Procedural languages, Program structures, Temporal safety properties
IdentifiersURN: urn:nbn:se:kth:diva-128950DOI: 10.1007/978-3-319-15317-9_20ScopusID: 2-s2.0-84922326750ISBN: 978-3-319-15316-2ISBN: 978-3-319-15317-9OAI: oai:DiVA.org:kth-128950DiVA: diva2:649033
11th International Symposium on Formal Aspects of Component Software, FACS 2014, Bertinoro, Italy, 10 September 2014 through 12 September 2014
QC 20150504. Updated from manuscript to conference paper.2013-09-172013-09-172015-05-04Bibliographically approved