swMATH6584MaRDI QIDQ18676FDOQ18676
Author name not available (Why is that?)
Official website: http://cl-informatik.uibk.ac.at/software/ceta/
Cited In (only showing first 100 items - show all)
- Modular complexity analysis for term rewriting
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- A Decision Procedure for Regular Expression Equivalence in Type Theory
- A framework for developing stand-alone certifiers
- Multi-dimensional interpretations for termination of term rewriting
- CSI: new evidence -- a progress report
- Proof pearl: A mechanized proof of GHC's mergesort
- Fast machine words in Isabelle/HOL
- NaTT
- A framework for the verification of certifying computations
- Proving termination by dependency pairs and inductive theorem proving
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Robinson arithmetic
- Proving termination of programs automatically with AProVE
- AC dependency pairs revisited
- AProVE
- Tyrolean
- CSI
- CoLoR
- CiME
- mkbTT
- Jambox
- MU-TERM
- IsaFoR
- Matchbox
- Slothrop
- Saigawa
- CoLL
- Ctrl
- KITTeL
- HOL-TestGen
- Proof Pearl: regular expression equivalence and relation algebra
- Formalizing complex plane geometry
- Formalizing Knuth-Bendix orders and Knuth-Bendix completion
- A learning-based fact selector for Isabelle/HOL
- A Perron-Frobenius theorem for deciding matrix growth
- Matrix Operations
- KBCV
- Fiat
- A3PAT
- ConCon
- Nagoya Termination Tool
- SparrowBerry
- WorkflowFM
- EasyInterface
- term-rewriting
- CoCoWeb
- Cops
- CAVA Automata Library
- Archive Formal Proofs
- Berlekamp Zassenhaus
- Dijkstra Shortest Path
- FinFuns
- Efficient Mergesort
- FORT
- Myhill-Nerode
- Logtk
- LLL Factorization
- Perron Frobenius
- Haskell Show Class
- Jinja not Java
- Nested Multisets
- Coccinelle
- Light-weight Containers
- LTL_to_GBA
- Decreasing Diagrams II
- Stream Fusion
- Stream Fusion Code
- Real_Impl
- Well Quasi Orders
- Verified LLL
- Maximum Cardinality Matching
- Tree Automata
- Xml
- Count Complex Roots
- Certification_Monads
- Linear Recurrences
- ShortestPath
- ProTeM
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Open Induction
- Saturation_Framework
- TcT
- From LCF to Isabelle/HOL
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- A Lambda-Free Higher-Order Recursive Path Order
- KBCV – Knuth-Bendix Completion Visualizer
- Proof certificates for equality reasoning
- Code generation via higher-order rewrite systems
- Animating the formalised semantics of a Java-like language
- Termination of Isabelle functions via termination of rewriting
- Reachability, confluence, and termination analysis with state-compatible automata
- Generalized and formalized uncurrying
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
- WANDA
- Stream Fusion for Isabelle’s Code Generator
- Tuple interpretations for termination of term rewriting
- Title not available (Why is that?)
- A Mechanized Proof of Higman’s Lemma by Open Induction
- A verified implementation of algebraic numbers in Isabelle/HOL
This page was built for software: CeTA
