Formalizing bounded increase

DOI10.1007/978-3-642-39634-2_19MaRDI QIDQ5327348zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

Cited in

(6)

• Formally proving size optimality of sorting networks
• Confluence of orthogonal term rewriting systems in the prototype verification system
• Formalizing size-optimal sorting networks: extracting a certified proof checker
• Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof
• Proving Termination by Bounded Increase
• Implementing field extensions of the form Q[sqrt(b)]

Describes a project that uses

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)