Treffer: Algorithmic verification of procedural programs in the presence of code variability

Title:
Algorithmic verification of procedural programs in the presence of code variability
Authors:
Soleimanifard, Siavash, Gurov, Dilian
Publisher Information:
KTH, Teoretisk datalogi, TCS 2015
Document Type:
E-Ressource Electronic Resource
Index Terms:
Algorithms, Computer software, Semantics, Algorithmic verification, Generic frameworks, Global properties, Independent components, New components, Procedural languages, Program structures, Temporal safety properties, Computer Sciences, Datavetenskap (datalogi), Conference paper, info:eu-repo/semantics/conferenceObject, text
DOI:
10.1007.978-3-319-15317-9_20
URL:
http://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-128950
Availability:
Open access content. Open access content
info:eu-repo/semantics/openAccess
Note:
application/pdf
English
Other Numbers:
UPE oai:DiVA.org:kth-128950
0000-0002-0074-8786
urn:isbn:978-3-319-15316-2
urn:isbn:978-3-319-15317-9
doi:10.1007/978-3-319-15317-9_20
Scopus 2-s2.0-84922326750
1234893189
Contributing Source:
UPPSALA UNIV LIBR
From OAIster®, provided by the OCLC Cooperative.
Accession Number:
edsoai.on1234893189
Database:
OAIster

Weitere Informationen

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.
QC 20150504. Updated from manuscript to conference paper.