Change search
ReferencesLink to record
Permanent link

Direct link
Composing Modal Properties of Programs with Procedures
INRIA Sophia Antipolis, France.
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-0074-8786
2009 (English)In: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, Vol. 203, no 7, 87-101 p.Article in journal (Refereed) Published
Abstract [en]

In component based software design, formal reasoning about programs has to be compositional, allowing global, program-wide properties to be inferred from the properties of its components. The present paper addresses the problem of compositional verification of behavioural control flow properties of sequential programs with procedures, expressed in a modal logic. We use as a starting point a maximal model based method previously developed by the authors, which assumes the local properties to be structural (rather than behavioural). To handle local behavioural properties, we propose the combination of the above method with a translation from behavioural properties to sets of structural ones. The present paper presents a direct solution for the logic, and prepares the ground for a translation for the considerably more expressive logic obtained by adding greatest fixed-point recursion.

Place, publisher, year, edition, pages
2009. Vol. 203, no 7, 87-101 p.
National Category
Computer and Information Science
URN: urn:nbn:se:kth:diva-50771DOI: 10.1016/j.entcs.2009.03.028ScopusID: 2-s2.0-63049111486OAI: diva2:462645
QC 20111208Available from: 2011-12-07 Created: 2011-12-07 Last updated: 2011-12-08Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Gurov, Dilian
By organisation
Theoretical Computer Science, TCS
In the same journal
Electronical Notes in Theoretical Computer Science
Computer and Information 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

Altmetric score

Total: 19 hits
ReferencesLink to record
Permanent link

Direct link