Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Program Models for Compositional Verification
KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.ORCID-id: 0000-0002-0074-8786
2008 (engelsk)Inngår i: FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, Berlin: Springer , 2008, s. 147-166Konferansepaper, Publicerat paper (Fagfellevurdert)
Abstract [en]

Compositional verification is crucial for guaranteeing the security of systems where new components can be loaded dynamically. In earlier work, we developed a compositional verification principle for control-flow properties of sequential control flow graphs with procedures. This paper discusses how the principle can be generalised to richer program models. We first present a generic program model, of which the original program model is an instantiation, and explicate under what conditions the compositional verification principle applies. We then present two other example instantiations of the generic model: with exceptional and with multi-threaded control flow, and show that for these particular instantiations the conditions hold. The program models we present are specifically tailored to our compositional verification principle, however, they are sufficiently intuitive and standard to be useful on their own. Tool support and practical application of the method are discussed.

sted, utgiver, år, opplag, sider
Berlin: Springer , 2008. s. 147-166
Serie
Lecture notes in computer science, ISSN 0302-9743 ; 5256
HSV kategori
Identifikatorer
URN: urn:nbn:se:kth:diva-13466ISI: 000261798200011Scopus ID: 2-s2.0-57049119160OAI: oai:DiVA.org:kth-13466DiVA, id: diva2:325439
Konferanse
10th International Conference on Formal Engineering Methods Kitakyushu-City, JAPAN, OCT 27-31, 2008
Merknad
QC 20100618Tilgjengelig fra: 2010-06-18 Laget: 2010-06-18 Sist oppdatert: 2018-01-12bibliografisk kontrollert

Open Access i DiVA

Fulltekst mangler i DiVA

Scopus

Personposter BETA

Gurov, Dilian

Søk i DiVA

Av forfatter/redaktør
Aktug, IremGurov, Dilian
Av organisasjonen

Søk utenfor DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric

urn-nbn
Totalt: 84 treff
RefereraExporteraLink to record
Permanent link

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