Modular termination verification

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

5 Citations (Scopus)
27 Downloads (Pure)

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.

Original languageEnglish
Title of host publication29th European Conference on Object-Oriented Programming, ECOOP 2015
EditorsJ.T. Boyland
PublisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik
Pages664-688
Number of pages25
Volume37
ISBN (Electronic)9783939897866
DOIs
Publication statusPublished - 1 Jul 2015
Event29th European Conference on Object-Oriented Programming, ECOOP 2015, 5-10 July 2015, Prague, Czech Republic - Prague, Czech Republic
Duration: 5 Jul 201510 Jul 2015
http://2015.ecoop.org/

Conference

Conference29th European Conference on Object-Oriented Programming, ECOOP 2015, 5-10 July 2015, Prague, Czech Republic
Abbreviated titleECOOP2015
CountryCzech Republic
CityPrague
Period5/07/1510/07/15
Internet address

Keywords

  • Modular verification
  • Program verification
  • Separation logic
  • Termination
  • Well-founded relations

Fingerprint

Dive into the research topics of 'Modular termination verification'. Together they form a unique fingerprint.

Cite this