Finding and certifying loops

DOI10.1007/978-3-642-11266-9_63MaRDI QIDQ3401124zbMATH OpenOpenAlexFDO

Authors Harald Zankl, Christian Sternagel, Dieter Hofbauer, Aart Middeldorp

Publication date 28 January 2010

Published in SOFSEM 2010: Theory and Practice of Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-11266-9_63

zbMATH Keywords

certificationnonterminationrewriting

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Certification of nontermination proofs
• Non-Looping String Rewriting
• Termination of string rewriting proved automatically
• Certification of Termination Proofs Using CeTA
• Implementation and Application of Automata

Cited in

(3)

• Loop detection by logically constrained term rewriting
• Lower bounds for runtime complexity of term rewriting
• Certification of nontermination proofs

Describes a project that uses

Uses Software

• Isabelle/HOL

This page was built for publication: Finding and certifying loops

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