The ITP tool is a theorem prover that can be used to prove properties of membership equational specifications, as well as incompletely specified algorithms on them, as a way to support incremental development of specifications. Membership equational logic is an expressive version of equational logic, particularly adequate for specifying and verifying semantic data structures, such as ordered lists, binary search trees, priority queues, and powerlists.

References in zbMATH (referenced in 16 articles )

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

  1. Skeirik, Stephen; Meseguer, José: Metalevel algorithms for variant satisfiability (2016)
  2. Bonacina, Maria Paola; Furbach, Ulrich; Sofronie-Stokkermans, Viorica: On first-order model-based reasoning (2015)
  3. Alpuente, María; Escobar, Santiago; Espert, Javier; Meseguer, José: A modular order-sorted equational generalization algorithm (2014)
  4. Bertolissi, Clara; Fernández, Maribel: A metamodel of access control for distributed environments: applications and properties (2014)
  5. Bouhoula, Adel; Jacquemard, Florent: Sufficient completeness verification for conditional and constrained TRS (2012)
  6. Durán, Francisco; Meseguer, José: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories (2012)
  7. Meseguer, José: Twenty years of rewriting logic (2012)
  8. Rocha, Camilo; Meseguer, José: Constructors, sufficient completeness, and deadlock freedom of rewrite theories (2010)
  9. Alpuente, María; Escobar, Santiago; Meseguer, José; Ojeda, Pedro: A modular equational generalization algorithm (2009)
  10. Alpuente, María; Escobar, Santiago; Meseguer, José; Ojeda, Pedro: Order-sorted generalization (2009)
  11. Clavel, Manuel; Durán, Francisco; Eker, Steven; Lincoln, Patrick; Martí-Oliet, Narciso; Meseguer, José; Talcott, Carolyn: All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM. (2007)
  12. Meseguer, José; Roşu, Grigore: The rewriting logic semantics project (2007)
  13. Rosa-Velardo, Fernando; Segura, Clara; Verdejo, Alberto: Typed mobile ambients in Maude (2006)
  14. Hendrix, Joe; Clavel, Manuel; Meseguer, José: A sufficient completeness reasoning tool for partial specifications (2005)
  15. Martí-Oliet, Narciso; Palomino, Miguel; Verdejo, Alberto: A tutorial on specifying data structures in Maude (2005)
  16. Meseguer, José: A rewriting logic sampler (2005)