DROPS

Document

DOI: 10.4230/LIPIcs.ECOOP.2015.664

Modular Termination Verification

Authors: Bart Jacobs, Dragan Bosnacki, and Ruurd Kuiper

Published in: LIPIcs, Volume 37, 29th European Conference on Object-Oriented Programming (ECOOP 2015)

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.

Cite as

Bart Jacobs, Dragan Bosnacki, and Ruurd Kuiper. Modular Termination Verification. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 664-688, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{jacobs_et_al:LIPIcs.ECOOP.2015.664,
  author =	{Jacobs, Bart and Bosnacki, Dragan and Kuiper, Ruurd},
  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 =	{Boyland, John Tang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.664},
  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}
}

Search Results

Documents authored by Bosnacki, Dragan

Modular Termination Verification

Abstract

Cite as

Thanks for your feedback!

Could not send message