Constructor-Based Inductive Theorem Prover

Constructor-Based Inductive Theorem Prover
复制标题

基于构造函数的归纳定理证明器

DOI：
10.1007/978-3-642-40206-7_26
复制
发表时间：
2013
期刊：
Proc. of the 5th International Conference on Algebra and Coalgebra in Computer Science (5th CALCO), LNCS 8089, Springer
影响因子：
--
通讯作者：
Yasuhito Arimoto
Yasuhito Arimoto
中科院分区：
--
文献类型：
--
作者：
Daniel Gaina;Min Zhang;Yuki Chiba;Yasuhito Arimoto

文献摘要

相似文献

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.