Change search
ReferencesLink to record
Permanent link

Direct link
Program Models for Compositional Verification
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-0074-8786
2008 (English)In: FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, Berlin: Springer , 2008, 147-166 p.Conference paper (Refereed)
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.

Place, publisher, year, edition, pages
Berlin: Springer , 2008. 147-166 p.
, Lecture notes in computer science, ISSN 0302-9743 ; 5256
National Category
Computer Science
URN: urn:nbn:se:kth:diva-13466ISI: 000261798200011ScopusID: 2-s2.0-57049119160OAI: diva2:325439
10th International Conference on Formal Engineering Methods Kitakyushu-City, JAPAN, OCT 27-31, 2008
QC 20100618Available from: 2010-06-18 Created: 2010-06-18 Last updated: 2012-03-19Bibliographically approved

Open Access in DiVA

No full text


Search in DiVA

By author/editor
Aktug, IremGurov, Dilian
By organisation
Theoretical Computer Science, TCS
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 41 hits
ReferencesLink to record
Permanent link

Direct link