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
Modular Specification and Verification
Karlsruhe Institute of Technology, Karlsruhe, Germany.
Technische Universität Darmstadt, Darmstadt, Germany.
Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). (MBT)
Karlsruhe Institute of Technology, Karlsruhe, Germany.
Show others and affiliations
2016 (English)In: Deductive Software Verification – The KeY Book: From Theory to Practice / [ed] Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt & Mattias Ulbrich, Heidelberg: Springer, 2016, p. 289-351Chapter in book (Other academic)
Abstract [en]

In this chapter, concepts already addressed in previous chapters are reconsidered and extended to cater for modularity. In particular, it is shown how method contracts can be used in proofs (as opposed to being verified themselves). Another central topic is nonfunctional framing information, i.e., information on what locations a method may write to or read from. But, there are also items that are discussed here in depth for the first time: model methods, an abstraction of Java methods that are only used in specification, verification of recursive methods, and object invariants. For any of the arising proof obligations the calculus rules needed to dispatch them are shown. © Springer International Publishing AG 2016.

Place, publisher, year, edition, pages
Heidelberg: Springer, 2016. p. 289-351
Series
Lecture Notes in Computer Science (LNCS), ISSN 0302-9743 ; 10001
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:hh:diva-35405DOI: 10.1007/978-3-319-49812-6_9Scopus ID: 2-s2.0-85006997785Libris ID: 19984323ISBN: 978-3-319-49811-9 (print)ISBN: 978-3-319-49812-6 (electronic)OAI: oai:DiVA.org:hh-35405DiVA, id: diva2:1156484
Available from: 2017-11-13 Created: 2017-11-13 Last updated: 2018-01-13Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records BETA

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
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 44 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