Certifying a Termination Criterion Based on Graphs, without Graphs

DOI10.1007/978-3-540-71067-7_17zbMath1165.68455OpenAlexW1498571906MaRDI QIDQ3543658

Pierre Courtieu, Xavier Urbain, Julien Forest

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)

Related Items (2)

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

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Mechanizing and improving dependency pairs
• Termination of term rewriting using dependency pairs
• Certification of Automated Termination Proofs
• Modeling Permutations in Coq for Coccinelle
• Proving innermost normalisation automatically
• Term Rewriting and All That
• Term Rewriting and Applications
• Automated Deduction – CADE-19
• Verification of Erlang processes by dependency pairs

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