Certification of nontermination proofs

DOI10.1007/978-3-642-32347-8_18MaRDI QIDQ2914748zbMATH OpenOpenAlexFDO

Authors Christian Sternagel, René Thiemann

Publication date 20 September 2012

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

Full work available at URL https://doi.org/10.1007/978-3-642-32347-8_18

zbMATH Keywords

formalizationinteractive theorem provingnonterminationterm rewriting

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Finding and certifying loops
• Certification of Termination Proofs Using CeTA
• Certification of Automated Termination Proofs
• Proving non-termination by finite automata
• Certification of complexity proofs using CeTA

Cited in

(12)

• Certifying safety and termination proofs for integer transition systems
• Certificates of Non-Membership for Classes of Read-Once Functions
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
• Certification of Termination Proofs Using CeTA
• Finding and certifying loops
• The Proof Certifier Checkers
• Deciding Innermost Loops
• Certification of Automated Termination Proofs
• Deterministic unimodularity certification
• Certification of complexity proofs using CeTA
• Certified subterm criterion and certified usable rules
• Building program construction and verification tools from algebraic principles

Describes a project that uses

Uses Software

• Isabelle/HOL

This page was built for publication: Certification of nontermination proofs

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