hh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • 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
From Explicit to Implicit Dynamic Frames in Concurrent Reasoning for Java
Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). (MBT)
2020 (English)In: Deductive Software Verification: Future Perspectives / [ed] Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Mattias Ulbrich, Heidelberg: Springer, 2020, p. 177-203Chapter in book (Refereed)
Abstract [en]

In our earlier work we presented a method for formal verification of concurrent Java programs based on Dynamic Logic and symbolic permissions. Embedded within the explicit dynamic frames method realised through JML⁎ specifications, permissions to heap locations and the actual heap location values are tracked separately and require two independent and often overlapping frame specifications. This is in contrast to well established Separation Logic and sibling frameworks, where program frames are inferred from permission annotations that already provide implicit framing information.

In this paper we show how to avoid redundant frame specifications and move towards the implicit framing approach in our method. We strive to keep as much as possible of the existing reasoning framework to preserve the general verification philosophy and implementation of our verification tool, the KeY verifier. We achieve our goal by only a small alteration of the existing proof obligation generation without changing any core part of the underlying logic, in particular, we maintain its closed character. However, even though specifications become more natural and less redundant, the indirect character of the specifications introduces a clear performance penalty for the verification engine.

We then proceed to a brief discussion why, under our minimal approach assumptions, this extension is still not sufficient to translate Separation Logic specifications into our framework. © 2020, Springer Nature Switzerland AG.

Place, publisher, year, edition, pages
Heidelberg: Springer, 2020. p. 177-203
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 12345
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:hh:diva-43704DOI: 10.1007/978-3-030-64354-6_7Scopus ID: 2-s2.0-85097580783OAI: oai:DiVA.org:hh-43704DiVA, id: diva2:1510159
Funder
Knowledge Foundation, 280034Available from: 2020-12-15 Created: 2020-12-15 Last updated: 2021-01-12Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Mostowski, Wojciech

Search in DiVA

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

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

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

Direct link
Cite
Citation style
  • apa
  • 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