Termination Competition (termCOMP 2015)

DOI10.1007/978-3-319-21401-6_6MaRDI QIDQ3454084zbMATH OpenOpenAlexFDO

Authors Jürgen Giesl, Frédéric Mesnard, Albert Rubio, René Thiemann, Johannes Waldmann

Publication date 2 December 2015

Published in Automated Deduction - CADE-25 (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/2117/85179

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Proving termination of programs automatically with AProVE
• Termination Analysis by Dependency Pairs and Inductive Theorem Proving
• Certification of complexity proofs using CeTA
• Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages

Cited in

(9)

• Automatic synthesis of logical models for order-sorted first-order theories
• Constant runtime complexity of term rewriting is semi-decidable
• A Perron-Frobenius theorem for deciding matrix growth
• A verified implementation of algebraic numbers in Isabelle/HOL
• Termination of cycle rewriting by transformation and matrix interpretation
• From Outermost to Context-Sensitive Rewriting
• A nesting-preserving transformation of SIMP programs into logically constrained term rewrite systems
• Find, use, and conserve tools for formal methods
• The Factorization Algorithm of Berlekamp and Zassenhaus

This page was built for publication: Termination Competition (termCOMP 2015)

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