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.