Change search
ReferencesLink to record
Permanent link

Direct link
ProMoVer: Modular Verification of Temporal 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)
2011 (English)In: Software Engineering and Formal Methods (SEFM) 2011, Springer , 2011, 366-381 p.Conference paper (Refereed)
Abstract [en]

This paper describes ProMoVer, a tool 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 at the procedure–level is a natural instantiation of the modular verification paradigm, where correctness ofglobal properties is relativized on the local properties of the methods rather than on their implementations, and is based here on the construction of maximal models for a program model that abstracts away from program data. This approach allows global properties to be verified in the presence of code evolution, multiple method implementations (as arising from software product lines), or even unknown method implementations (as in mobile code for open platforms). ProMoVer automates a typical verification scenario for a previously developed tool set for compositionalverification of control flow safety properties, and provides appropriatepre– and post–processing. Modularity is exploited by a mechanism for proof reuse that detects and minimizes the verfication tasks resulting from changes in the code and the specifications. The verification task is relatively light–weight due to support for abstraction from private methods and automatic extraction of candidate specifications from methodimplementations. We evaluate the tool on a number of applications from the smart card domain.

Place, publisher, year, edition, pages
Springer , 2011. 366-381 p.
, Lecture notes in computer science, ISSN 0302-9743 ; 7041
National Category
Computer Science
URN: urn:nbn:se:kth:diva-49416DOI: 10.1007/978-3-642-24690-6ISI: 000305321300025ScopusID: 2-s2.0-81055124334ISBN: 978-3-642-24689-0OAI: diva2:459633
9th International Conference, SEFM 2011, Montevideo, Uruguay, November 14-18, 2011

QC 20120111

Available from: 2012-01-11 Created: 2011-11-27 Last updated: 2013-04-29Bibliographically approved

Open Access in DiVA

final_version(383 kB)95 downloads
File information
File name FULLTEXT01.pdfFile size 383 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Other links

Publisher's full textScopusConference website“The final publication is available at”

Search in DiVA

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

Search outside of DiVA

GoogleGoogle Scholar
Total: 95 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: 45 hits
ReferencesLink to record
Permanent link

Direct link