Constructor-based inductive theorem prover. Constructor-based theorem prover (CITP) is a tool for proving inductive properties of software systems specified with constructor-based logics. CITP is equipped with a default proof strategy for the automated verification of observational transitional systems (OTS), but the area of applications is not restricted to OTS. The proof strategy can be customised by the user, or the basic tactics can be applied step-by-step. The tool features are exhibited on concrete examples, showing how to perform verification with CITP.
Keywords for this software
References in zbMATH (referenced in 7 articles , 1 standard article )
Showing results 1 to 7 of 7.
- Găină, Daniel; Nakamura, Masaki; Ogata, Kazuhiro; Futatsugi, Kokichi: Stability of termination and sufficient-completeness under pushouts via amalgamation (2020)
- Zhang, Min; Ogata, Kazuhiro: From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories (2018)
- Riesco, Adrián; Ogata, Kazuhiro; Futatsugi, Kokichi: A Maude environment for CafeOBJ (2017)
- Găină, Daniel; Lucanu, Dorel; Ogata, Kazuhiro; Futatsugi, Kokichi: On automation of OTS/CafeOBJ method (2014)
- Ogata, Kazuhiro; Futatsugi, Kokichi: Theorem proving based on proof scores for rewrite theory specifications of OTSs (2014)
- Rocha, Camilo; Meseguer, José: Mechanical analysis of reliable communication in the alternating bit protocol using the Maude invariant analyzer tool (2014)
- Găină, Daniel; Zhang, Min; Chiba, Yuki; Arimoto, Yasuhito: Constructor-based inductive theorem prover (2013)