Proving mutual termination

DOI10.1007/S10703-015-0234-3MaRDI QIDQ746783zbMATHOpenAlexFDO

Authors Dima Elenbogen, Shmuel Katz, Ofer Strichman

Publication date 20 October 2015

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10703-015-0234-3

zbMATH Keywords

program terminationmutual terminationregression-verification

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Termination of nested and mutually recursive algorithms
• Termination proofs for logic programs
• Mechanical verification of mutually recursive procedures
• Inference rules for proving the equivalence of recursive procedures
• Secure mechanical verification of mutually recursive procedures

Cites work

• scientific article; zbMATH DE number 3688740 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• scientific article; zbMATH DE number 3351180 (Why is no real title available?)
• Computer Aided Verification
• Inference rules for proving the equivalence of recursive procedures
• On the Collatz 3n + 1 Algorithm
• Static Analysis
• Towards modularly comparing programs using automated theorem provers

Cited in

(3)

• Modular verification of procedure equivalence in the presence of memory allocation
• Mechanical verification of mutually recursive procedures
• Verifying relative safety, accuracy, and termination for program approximations

Describes a project that uses

Uses Software

• Boogie
• GitHub

This page was built for publication: Proving mutual termination

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q746783)