ITP

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 31 articles )

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

1 2 next

  1. Durán, Francisco; Eker, Steven; Escobar, Santiago; Martí-Oliet, Narciso; Meseguer, José; Rubio, Rubén; Talcott, Carolyn: Programming and symbolic computation in Maude (2020)
  2. Lucas, Salvador: Proving semantic properties as first-order satisfiability (2019)
  3. Skeirik, Stephen; Meseguer, José: Metalevel algorithms for variant satisfiability (2018)
  4. Zhang, Min; Ogata, Kazuhiro: From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories (2018)
  5. Skeirik, Stephen; Meseguer, José: Metalevel algorithms for variant satisfiability (2016)
  6. Bonacina, Maria Paola; Furbach, Ulrich; Sofronie-Stokkermans, Viorica: On first-order model-based reasoning (2015)
  7. Alpuente, María; Escobar, Santiago; Espert, Javier; Meseguer, José: A modular order-sorted equational generalization algorithm (2014)
  8. Bertolissi, Clara; Fernández, Maribel: A metamodel of access control for distributed environments: applications and properties (2014)
  9. Bouhoula, Adel; Jacquemard, Florent: Sufficient completeness verification for conditional and constrained TRS (2012)
  10. Durán, Francisco; Meseguer, José: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories (2012)
  11. Futatsugi, Kokichi; Găină, Daniel; Ogata, Kazuhiro: Principles of proof scores in CafeOBJ (2012)
  12. Meseguer, José: Twenty years of rewriting logic (2012)
  13. Codescu, Mihai; Mossakowski, Till; Riesco, Adrián; Maeder, Christian: Integrating Maude into Hets (2011)
  14. Meseguer, José; Palomino, Miguel; Martí-Oliet, Narciso: Algebraic simulations (2010)
  15. Rocha, Camilo; Meseguer, José: Constructors, sufficient completeness, and deadlock freedom of rewrite theories (2010)
  16. Alpuente, María; Escobar, Santiago; Meseguer, José; Ojeda, Pedro: Order-sorted generalization (2009)
  17. Alpuente, María; Escobar, Santiago; Meseguer, José; Ojeda, Pedro: A modular equational generalization algorithm (2009)
  18. Durán, Francisco; Ölveczky, Peter Csaba: A guide to extending Full Maude illustrated with the implementation of real-time Maude (2009) ioport
  19. Holen, Bjarne; Johnsen, Einar Broch; Waaler, Arild: Proof search for the first-order connection calculus in Maude (2009)
  20. Meseguer, José; Palomino, Miguel; Martí-Oliet, Narciso: Equational abstractions (2008)

1 2 next