CiME

CiME is a rewriting toolbox. Distributed since 1996 as open source, at URL http://cime.lri.fr . Beyond a few dozens of users, CiME is used as back-end for other tools such as the TALP tool developed by Enno Ohlebusch at Bielefeld university for termination of logic programs; the MU-TERM tool (http://www.dsic.upv.es/ slucas/csr/termination/muterm/ ) for termination of context-sensitive rewriting; the CARIBOO tool (developed at INRIA Nancy Grand-Est) for termination of rewriting under strategies; and the MTT tool (http://www.lcc.uma.es/ duran/MTT/ ) for termination of Maude programs. CiME2 is no longer maintained, and the currently developed version is CiME3, available at http://a3pat.ensiie.fr/pub . The main new feature of CiME3 is the production of traces for Coq. CiME3 is also developed by the participants of the A3PAT project at the CNAM, and is distributed under the Cecill-C licence.


References in zbMATH (referenced in 38 articles )

Showing results 1 to 20 of 38.
Sorted by year (citations)

1 2 next

  1. Hirokawa, Nao; Middeldorp, Aart; Sternagel, Christian; Winkler, Sarah: Abstract completion, formalized (2019)
  2. Ayala-Rincón, Mauricio; Fernández, Maribel; Nantes-Sobrinho, Daniele: Intruder deduction problem for locally stable theories with normal forms and inverses (2017)
  3. Blanchette, Jasmin Christian; Waldmann, Uwe; Wand, Daniel: A lambda-free higher-order recursive path order (2017)
  4. Cruz-Filipe, Luís; Larsen, Kim S.; Schneider-Kamp, Peter: Formally proving size optimality of sorting networks (2017)
  5. Giesl, Jürgen; Aschermann, Cornelius; Brockschmidt, Marc; Emmes, Fabian; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Otto, Carsten; Plücker, Martin; Schneider-Kamp, Peter; Ströder, Thomas; Swiderski, Stephanie; Thiemann, René: Analyzing program termination and complexity automatically with \textsfAProVE (2017)
  6. McCabe-Dansted, John C.; Reynolds, Mark: Rewrite rules for (\mathrmCTL^\ast) (2017)
  7. Nagele, Julian; Felgenhauer, Bertram; Zankl, Harald: Certifying confluence proofs via relative termination and rule labeling (2017)
  8. Ströder, Thomas; Giesl, Jürgen; Brockschmidt, Marc; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Schneider-Kamp, Peter; Aschermann, Cornelius: Automatically proving termination and memory safety for programs with pointer arithmetic (2017)
  9. Nagele, Julian; Middeldorp, Aart: Certification of classical confluence results for left-linear term rewrite systems (2016)
  10. Cruz-Filipe, Luís; Schneider-Kamp, Peter: Optimizing a certified proof checker for a large-scale computer-generated proof (2015)
  11. Nagele, Julian; Felgenhauer, Bertram; Middeldorp, Aart: Improving automatic confluence analysis of rewrite systems by redundant rules (2015)
  12. Nagele, Julian; Zankl, Harald: Certified rule labeling (2015)
  13. Giesl, Jürgen; Brockschmidt, Marc; Emmes, Fabian; Frohn, Florian; Fuhs, Carsten; Otto, Carsten; Plücker, Martin; Schneider-Kamp, Peter; Ströder, Thomas; Swiderski, Stephanie; Thiemann, René: Proving termination of programs automatically with AProVE (2014)
  14. Babić, Domagoj; Cook, Byron; Hu, Alan J.; Rakamarić, Zvonimir: Proving termination of nonlinear command sequences (2013)
  15. Bouhoula, Adel; Jacquemard, Florent: Sufficient completeness verification for conditional and constrained TRS (2012)
  16. Bosser, Anne-Gwenn; Courtieu, Pierre; Forest, Julien; Cavazza, Marc: Structural analysis of narratives with the Coq proof assistant (2011)
  17. Contejean, Évelyne; Courtieu, Pierre; Forest, Julien; Pons, Olivier; Urbain, Xavier: Automated certified proofs with CiME3 (2011)
  18. Zankl, Harald; Felgenhauer, Bertram; Middeldorp, Aart: CSI -- a confluence tool (2011)
  19. Baudet, Mathieu; Cortier, Véronique; Kremer, Steve: Computationally sound implementations of equational theories against passive adversaries (2009)
  20. Borralleras, Cristina; Lucas, Salvador; Navarro-Marset, Rafael; Rodríguez-Carbonell, Enric; Rubio, Albert: Solving non-linear polynomial arithmetic via SAT modulo linear arithmetic (2009)

1 2 next