Document Open Access Logo

Modular Termination Verification

Authors Bart Jacobs, Dragan Bosnacki, Ruurd Kuiper

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2015.664.pdf
  • Filesize: 0.54 MB
  • 25 pages

Document Identifiers

Author Details

Bart Jacobs
Dragan Bosnacki
Ruurd Kuiper

Cite As Get BibTex

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) https://doi.org/10.4230/LIPIcs.ECOOP.2015.664

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.

Subject Classification

Keywords
  • Termination
  • program verification
  • modular verification
  • separation logic
  • well-founded relations

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Ádám Darvas and Peter Müller. Reasoning about method calls in interface specifications. Journal of Object Technology, 5(5):59-85, 2006. Google Scholar
  2. Samin S. Ishtiaq and Peter W. O'Hearn. BI as an assertion language for mutable data structures. In POPL, 2001. Google Scholar
  3. Bart Jacobs, Dragan Bosnacki, and Ruurd Kuiper. Modular termination verification: extended version. Technical Report CW 680, Dept. Comp. Sci., KU Leuven, 2015. Google Scholar
  4. Daan Leijen. Koka: Programming with row polymorphic effect types. In Mathematically Structured Functional Programming, 2014. Google Scholar
  5. K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In LPAR, 2010. Google Scholar
  6. K. Rustan M. Leino and Ronald Middelkoop. Proving consistency of pure methods and model fields. In FASE, 2009. Google Scholar
  7. K. Rustan M. Leino, Peter Müller, and Jan Smans. Deadlock-free channels and locks. In ESOP, 2010. Google Scholar
  8. Keiko Nakata and Tarmo Uustalu. Trace-based coinductive operational semantics for While. In TPHOLs, 2009. Google Scholar
  9. Peter W. O'Hearn, John C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In CSL, 2001. Google Scholar
  10. Matthew J. Parkinson and Gavin M. Bierman. Separation logic and abstraction. In POPL, 2005. Google Scholar
  11. Matthew J. Parkinson and Gavin M. Bierman. Separation logic, abstraction and inheritance. In POPL, 2008. Google Scholar
  12. Arsenii Rudich, Ádám Darvas, and Peter Müller. Checking well-formedness of pure-method specifications. In FM, 2008. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact