Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Reports, Documentation, and Standards
  4. Proving Termination via Measure Transfer in Equivalence Checking (Extended Version)
 
technical report

Proving Termination via Measure Transfer in Equivalence Checking (Extended Version)

Milovančević, Dragana  
•
Fuhs, Carsten
•
Bucev, Mario  
Show more
September 19, 2024

Program verification can benefit from proofs with varied induction schemas. A natural class of induction schemas, functional induction, consists of those derived from definitions of functions. For such inductive proofs to be sound, it is necessary to establish that the functions terminate, which is a challenging problem on its own. In this paper, we consider termination in the context of equivalence checking of a candidate program against a provably terminating reference program annotated with termination measures. Using equivalence checking, our approach automatically matches function calls in the reference and candidate programs and proves termination by transferring measures from a measure-annotated program to one without annotations. We evaluate this approach on existing and newly written termination benchmarks, as well as on exercises in programming courses. Our evaluation corpus comprises around 10K lines of code. We show empirically that the termination measures of reference programs often successfully prove the termination of equivalent candidate programs, ensuring the soundness of inductive reasoning in a fully automated manner.

  • Files
  • Details
  • Metrics
Type
technical report
Author(s)
Milovančević, Dragana  

École Polytechnique Fédérale de Lausanne

Fuhs, Carsten

Birkbeck, University of London

Bucev, Mario  

EPFL

Kuncak, Viktor  orcid-logo

EPFL

Date Issued

2024-09-19

Subjects

Equivalence checking

•

Termination analysis

•

Termination measures

Note

This technical report is an extended version of our iFM’24 paper: Proving Termination via Measure Transfer in Equivalence Checking.

Editorial or Peer reviewed

NON-REVIEWED

Written at

EPFL

EPFL units
LARA  
RelationRelated workURL/DOI

IsCitedBy

Proving Termination via Measure Transfer in Equivalence Checking

https://infoscience.epfl.ch/handle/20.500.14299/240394
Available on Infoscience
September 20, 2024
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/241339
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés