hh.sePublications
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
Dynamic Frames Based Verification Method for Concurrent Java Programs
Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). University of Twente, Enschede, The Netherlands. (Model Based Testing)
2016 (English)In: Verified Software: Theories, Tools, and Experiments: 7th International Conference, VSTTE 2015, San Francisco, CA, USA, July 18-19, 2015. Revised Selected Papers / [ed] Arie Gurfinkel & Sanjit A. Seshia, New York: Springer International Publishing Switzerland , 2016, Vol. 9593, 124-141 p.Conference paper, (Refereed)
Abstract [en]

In this paper we discuss a verification method for concurrent Java programs based on the concept of dynamic frames. We build on our earlier work that proposes a new, symbolic permission system for concurrent reasoning and we provide the following new contributions. First, we describe our approach for proving program specifications to be self-framed w.r.t. permissions, which is a necessary condition to maintain soundness in concurrent reasoning. Second, we show how we use predicates to provide modular and reusable specifications for program synchronisation points, like locks or forked threads. Our work primarily targets the KeY verification system with its specification language JML* and symbolic execution proving method. Hence, we also give the current status of the work on implementation and we discuss some examples that are verifiable with KeY. © Springer International Publishing Switzerland 2016

Place, publisher, year, edition, pages
New York: Springer International Publishing Switzerland , 2016. Vol. 9593, 124-141 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9593
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:hh:diva-30171DOI: 10.1007/978-3-319-29613-5_8ISBN: 978-3-319-29612-8 (print)ISBN: 978-3-319-29613-5 (print)OAI: oai:DiVA.org:hh-30171DiVA: diva2:894284
Conference
7th International Conference, VSTTE 2015, San Francisco, CA, USA, July 18-19, 2015
Projects
VerCorsAUTO-CAAS
Funder
Knowledge Foundation
Note

This work is supported by ERC grant 258405 for the VerCors project and by the Swedish Knowledge Foundation grant for the AUTO-CAAS project.

Available from: 2016-01-14 Created: 2016-01-14 Last updated: 2017-03-07Bibliographically approved

Open Access in DiVA

fulltext(995 kB)11 downloads
File information
File name FULLTEXT01.pdfFile size 995 kBChecksum SHA-512
fc21ef41b954b9a81c92fde7cf0c4682588e193e734dad5957c615b27870860d63ae6dfe3c30c510b7b98fa2a42ccd7a8165d4f76adf054c854e51b70b55260b
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Search in DiVA

By author/editor
Mostowski, Wojciech
By organisation
Centre for Research on Embedded Systems (CERES)
Computer Systems

Search outside of DiVA

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