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
Algorithmic verification of procedural programs in the presence of code variability
2016 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 127, 76-102 p.Article in journal (Refereed) Published
Resource type
Text
Abstract [en]

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 fully abstracts from program data. In this work, we recapture 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 behaviour it induces to facilitate independent component specification and verification. To exemplify the use of the framework, we develop three concrete instantiations; in particular, we derive a compositional verification technique for programs written in a procedural language with pointers as the only datatype.

Place, publisher, year, edition, pages
Elsevier, 2016. Vol. 127, 76-102 p.
Keyword [en]
Compositional verification, Model checking, Maximal models
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:kth:diva-190634DOI: 10.1016/j.scico.2015.08.010ISI: 000379282600005Scopus ID: 2-s2.0-84971665264OAI: oai:DiVA.org:kth-190634DiVA: diva2:953910
Note

QC 20160819

Available from: 2016-08-19 Created: 2016-08-12 Last updated: 2016-08-19Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus
In the same journal
Science of Computer Programming
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 7 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