Formalizing bounded increase

DOI10.1007/978-3-642-39634-2_19zbMATH Open1317.68233OpenAlexW1840129892MaRDI QIDQ5327348FDOQ5327348

Authors: René Thiemann 

Publication date: 7 August 2013

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-39634-2_19

Recommendations

• Proving Termination by Bounded Increase
• scientific article; zbMATH DE number 107881
• Computer Aided Verification
• Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
• scientific article; zbMATH DE number 4072437

Mathematics Subject Classification ID

Cited In (5)

• Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof
• Confluence of orthogonal term rewriting systems in the prototype verification system
• Formalizing size-optimal sorting networks: extracting a certified proof checker
• Formally proving size optimality of sorting networks
• Proving Termination by Bounded Increase

Uses Software

• Isabelle/HOL

This page was built for publication: Formalizing bounded increase

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