Change search
ReferencesLink to record
Permanent link

Direct link
Procedure-Modular Verification of Control Flow Safety Properties
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
University of Twente. (Formal Methods and Tools)
2010 (English)In: Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs, 2010Conference paper (Refereed)
Abstract [en]

This paper describes a novel technique for fully automated procedure–modular verification of Java programs equipped with method–local and global assertions that specify safety properties of sequences of method invocations. Modularity of verification is achieved by relativizing the correctness of global properties on the local properties rather than on the implementations of methods, and is based on the construction of maximal models. Tool support is provided by means of ProMoVer, a tool that is essentially a wrapper around a previously developed tool set for compositional verification of control flow safety properties, where program data is abstracted a way completely. We evaluate the technique on a small but realistic case study.

Place, publisher, year, edition, pages
Keyword [en]
Maximal models, Modular verification, Temporal logic
National Category
Computer and Information Science
URN: urn:nbn:se:kth:diva-38455DOI: 10.1145/1924520.1924525ScopusID: 2-s2.0-79957970909ISBN: 978-1-4503-0540-2OAI: diva2:436901
12th Workshop on Formal Techniques for Java-like Programs, June 22, Maribor (Slovenia
QC 20110826Available from: 2011-08-26 Created: 2011-08-25 Last updated: 2011-08-26Bibliographically approved

Open Access in DiVA

ftfjp2010.pdf(243 kB)31 downloads
File information
File name FULLTEXT01.pdfFile size 243 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Other links

Publisher's full textScopusECOOP 2010

Search in DiVA

By author/editor
Soleimanifard, SiavashGurov, Dilian
By organisation
Theoretical Computer Science, TCS
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 31 downloads
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: 63 hits
ReferencesLink to record
Permanent link

Direct link