swMATH ID: 9808
Software Authors: Clavel, M.; Palomino, M.; Riesco, A.
Description: 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.
Homepage: http://maude.sip.ucm.es/itp/
Dependencies: Maude
Related Software: Maude; SCC; CafeOBJ; OBJ3; PMaude; MTT; JavaFAN; MFE; Stratego; MMT; ACL2; AProVE; Maude-NPA; Mace4; SPIN; CASL; LETOS; CRC 3; Java+ITP; CARIBOO
Referenced in: 29 Publications

Referencing Publications by Year