kth.sePublikationer
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Algorithmic verification of procedural programs in the presence of code variability
KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.ORCID-id: 0000-0002-0074-8786
2016 (Engelska)Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 127, s. 76-102Artikel i tidskrift (Refereegranskat) Published
Resurstyp
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.

Ort, förlag, år, upplaga, sidor
Elsevier, 2016. Vol. 127, s. 76-102
Nyckelord [en]
Compositional verification, Model checking, Maximal models
Nationell ämneskategori
Datorsystem
Identifikatorer
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, id: diva2:953910
Anmärkning

QC 20160819

Tillgänglig från: 2016-08-19 Skapad: 2016-08-12 Senast uppdaterad: 2022-06-22Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltextScopus

Person

Soleimanifard, SiavashGurov, Dilian

Sök vidare i DiVA

Av författaren/redaktören
Soleimanifard, SiavashGurov, Dilian
Av organisationen
KTHTeoretisk datalogi, TCS
I samma tidskrift
Science of Computer Programming
Datorsystem

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetricpoäng

doi
urn-nbn
Totalt: 45 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf