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
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, Published 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
2010.
Keyword [en]
Maximal models, Modular verification, Temporal logic
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:kth:diva-38455DOI: 10.1145/1924520.1924525Scopus ID: 2-s2.0-79957970909ISBN: 978-1-4503-0540-2 (print)OAI: oai:DiVA.org:kth-38455DiVA: diva2:436901
Conference
12th Workshop on Formal Techniques for Java-like Programs, June 22, Maribor (Slovenia
Note
QC 20110826Available from: 2011-08-26 Created: 2011-08-25 Last updated: 2011-08-26Bibliographically approved

Open Access in DiVA

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

Other links

Publisher's full textScopusECOOP 2010

Authority records BETA

Gurov, Dilian

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: 44 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: 78 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