swMATH9970MaRDI QIDQ21947FDOQ21947
Author name not available (Why is that?)
Official website: https://raweb.inria.fr/rapportsactivite/RA2010/proval/uid32.html
Cited In (65)
- WANDA
- Intruder deduction problem for locally stable theories with normal forms and inverses
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- Tuple interpretations for termination of term rewriting
- Towards Rewriting in Coq
- Title not available (Why is that?)
- Certification of Proving Termination of Term Rewriting by Matrix Interpretations
- Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof
- Proving operational termination of membership equational programs
- Rewrite systems for natural, integral, and rational arithmetic
- CSI -- a confluence tool
- Automated certified proofs with CiME3
- Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
- Automated Deduction – CADE-20
- Polynomials over the reals in proofs of termination : from theory to practice
- Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
- Structural analysis of narratives with the Coq proof assistant
- On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting
- Proving termination of context-sensitive rewriting by transformation
- Term Rewriting and Applications
- Certifying a Termination Criterion Based on Graphs, without Graphs
- Mechanically proving termination using polynomial interpretations
- Computationally sound implementations of equational theories against passive adversaries
- Certified rule labeling
- Proving termination of programs automatically with AProVE
- Certifying confluence proofs via relative termination and rule labeling
- Certification of classical confluence results for left-linear term rewrite systems
- CeTA
- Proving termination of nonlinear command sequences
- AProVE
- Tyrolean
- CSI
- CoLoR
- CARIBOO
- Jambox
- MU-TERM
- IsaFoR
- Matchbox
- Saigawa
- TPDB
- TPA
- TORPA
- Tsukuba
- CoLL
- Ctrl
- KITTeL
- Nagoya Termination Tool
- STORM
- CoCoWeb
- Cops
- Coccinelle
- REVE
- Decreasing Diagrams II
- Well Quasi Orders
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Sufficient completeness verification for conditional and constrained TRS
- Abstract completion, formalized
- A Lambda-Free Higher-Order Recursive Path Order
- On tree automata that certify termination of left-linear term rewriting systems
- Modular and incremental proofs of AC-termination
- Formally proving size optimality of sorting networks
- Termination of just/fair computations in term rewriting
- Rewrite rules for \(\mathrm{CTL}^\ast\)
- Termination of string rewriting proved automatically
- Rewriting Techniques and Applications
This page was built for software: CiME
