License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2015.664
URN: urn:nbn:de:0030-drops-52422
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5242/
Go to the corresponding LIPIcs Volume Portal

Jacobs, Bart ; Bosnacki, Dragan ; Kuiper, Ruurd

Modular Termination Verification

pdf-format:
32.pdf (0.5 MB)

Abstract

We propose an approach for the modular specification and verification of total correctness properties of object-oriented programs. We start from an existing program logic for partial correctness based on separation logic and abstract predicate families. We extend it with call permissions qualified by an arbitrary ordinal number, and we define a specification style that properly hides implementation details, based on the ideas of using methods and bags of methods as ordinals, and exposing the bag of methods reachable from an object as an abstract predicate argument. These enable each method to abstractly request permission to call all methods reachable by it any finite number of times, and to delegate similar permissions to its callees. We illustrate the approach with several examples.

BibTeX - Entry

@InProceedings{jacobs_et_al:LIPIcs:2015:5242,
  author =	{Bart Jacobs and Dragan Bosnacki and Ruurd Kuiper},
  title =	{{Modular Termination Verification}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{664--688},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{John Tang Boyland},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5242},
  URN =		{urn:nbn:de:0030-drops-52422},
  doi =		{10.4230/LIPIcs.ECOOP.2015.664},
  annote =	{Keywords: Termination, program verification, modular verification, separation logic, well-founded relations}
}

Keywords: Termination, program verification, modular verification, separation logic, well-founded relations
Collection: 29th European Conference on Object-Oriented Programming (ECOOP 2015)
Issue Date: 2015
Date of publication: 29.06.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI