CiME
From MaRDI portal
Software:21947
No author found.
Related Items (38)
Analyzing program termination and complexity automatically with \textsf{AProVE} ⋮ Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Unnamed Item ⋮ Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof ⋮ Termination of string rewriting proved automatically ⋮ Mechanically proving termination using polynomial interpretations ⋮ Modular and incremental proofs of AC-termination ⋮ Proving termination of context-sensitive rewriting by transformation ⋮ Proving Termination of Programs Automatically with AProVE ⋮ Polynomials over the reals in proofs of termination : from theory to practice ⋮ On tree automata that certify termination of left-linear term rewriting systems ⋮ Unnamed Item ⋮ Rewrite systems for natural, integral, and rational arithmetic ⋮ Formally proving size optimality of sorting networks ⋮ Sufficient completeness verification for conditional and constrained TRS ⋮ Slothrop: Knuth-Bendix Completion with a Modern Termination Checker ⋮ Unnamed Item ⋮ Termination of just/fair computations in term rewriting ⋮ A Lambda-Free Higher-Order Recursive Path Order ⋮ Proving termination of nonlinear command sequences ⋮ Certifying a Termination Criterion Based on Graphs, without Graphs ⋮ Automated Deduction – CADE-20 ⋮ Term Rewriting and Applications ⋮ Intruder deduction problem for locally stable theories with normal forms and inverses ⋮ Rewrite rules for \(\mathrm{CTL}^\ast\) ⋮ Certified Rule Labeling ⋮ Proving operational termination of membership equational programs ⋮ Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic ⋮ On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting ⋮ Towards Rewriting in Coq ⋮ Certification of Proving Termination of Term Rewriting by Matrix Interpretations ⋮ CSI – A Confluence Tool ⋮ Computationally sound implementations of equational theories against passive adversaries ⋮ Structural Analysis of Narratives with the Coq Proof Assistant ⋮ Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems ⋮ Unnamed Item ⋮ Rewriting Techniques and Applications ⋮ Tuple interpretations for termination of term rewriting
This page was built for software: CiME
