CeTA
From MaRDI portal
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)
- 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
- Deriving comparators and show functions in Isabelle/HOL
- Modular and certified semantic labeling and unlabeling
- Certified rule labeling
- Certifying confluence proofs via relative termination and rule labeling
- Certification of classical confluence results for left-linear term rewrite systems
- Certification of complexity proofs using CeTA
- Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems
- Certifying safety and termination proofs for integer transition systems
- Abstract completion, formalized
- Automatic refinement to efficient data structures: a comparison of two approaches
- Certified subterm criterion and certified usable rules
- 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
This page was built for software: CeTA
