Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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, Published 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.
Series
Lecture notes in computer science, ISSN 0302-9743 ; 7041
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-49416DOI: 10.1007/978-3-642-24690-6ISI: 000305321300025Scopus ID: 2-s2.0-81055124334ISBN: 978-3-642-24689-0 (print)OAI: oai:DiVA.org:kth-49416DiVA: diva2:459633
Conference
9th International Conference, SEFM 2011, Montevideo, Uruguay, November 14-18, 2011
Note

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)120 downloads
File information
File name FULLTEXT01.pdfFile size 383 kBChecksum SHA-512
bba2466a66178944ee97e2b063774a00c9ab9f552a25fb645169110de951b8db677cdbf43f519041921b8119ddcfa49da1a2c614813e983ab4aae5c94b548ef0
Type fulltextMimetype application/pdf

Other links

Publisher's full textScopusConference website“The final publication is available at www.springerlink.com”

Authority records BETA

Gurov, Dilian

Search in DiVA

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

Search outside of DiVA

GoogleGoogle Scholar
Total: 120 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

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 55 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf