Proving mutual termination

DOI10.1007/s10703-015-0234-3zbMath1322.68052OpenAlexW2177439807MaRDI QIDQ746783

Dima Elenbogen, Ofer Strichman, Shmuel Katz

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

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

Related Items (2)

Modular Verification of Procedure Equivalence in the Presence of Memory Allocation ⋮ Verifying relative safety, accuracy, and termination for program approximations

Uses Software

• Boogie
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Inference rules for proving the equivalence of recursive procedures
• On the Collatz 3n + 1 Algorithm
• Towards Modularly Comparing Programs Using Automated Theorem Provers
• Computer Aided Verification
• Static Analysis

This page was built for publication: Proving mutual termination