Proving mutual termination

DOI10.1007/S10703-015-0234-3zbMATH Open1322.68052OpenAlexW2177439807MaRDI QIDQ746783FDOQ746783

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

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

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Static Analysis
• Inference rules for proving the equivalence of recursive procedures
• Towards modularly comparing programs using automated theorem provers
• Computer Aided Verification
• On the Collatz 3n + 1 Algorithm
• Title not available (Why is that?)

Cited In (3)

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

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)