Certifying a Termination Criterion Based on Graphs, without Graphs

DOI10.1007/978-3-540-71067-7_17MaRDI QIDQ3543658zbMATH OpenOpenAlexFDO

Authors Pierre Courtieu, Julien Forest, Xavier Urbain

Publication date 4 December 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-71067-7_17

Mathematics Subject Classification ID

Graph theory (including graph drawing) in computer science (68R10)

Recommendations

• Tools and Algorithms for the Construction and Analysis of Systems
• Towards a systematic method for proving termination of graph transformation systems
• On proving termination of constrained term rewrite systems by eliminating edges from dependency graphs
• Reachability predicates for graph assertions
• scientific article; zbMATH DE number 2242587
• scientific article; zbMATH DE number 1183250
• Certifying coloring algorithms for graphs without long induced paths
• Non-simplifying graph rewriting termination
• scientific article; zbMATH DE number 2016070
• Termination analysis for graph transformation systems

Cites work

• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 1487842 (Why is no real title available?)
• Automating the dependency pair method.
• Certification of Automated Termination Proofs
• Mechanizing and improving dependency pairs
• Modeling Permutations in Coq for Coccinelle
• Proving innermost normalisation automatically
• Term Rewriting and All That
• Term Rewriting and Applications
• Termination of term rewriting using dependency pairs
• Verification of Erlang processes by dependency pairs

Cited in

(2)

• Certification of Termination Proofs Using CeTA
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates

Describes a project that uses

Uses Software

• Coccinelle
• Jambox
• CiME
• CoLoR
• AProVE
• Tyrolean
• Coq

This page was built for publication: Certifying a Termination Criterion Based on Graphs, without Graphs

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