TY - GEN
T1 - Constructor-based inductive theorem prover
AU - Gǎinǎ, Daniel
AU - Zhang, Min
AU - Chiba, Yuki
AU - Arimoto, Yasuhito
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/84885981750
U2 - 10.1007/978-3-642-40206-7-26
DO - 10.1007/978-3-642-40206-7-26
M3 - 会议稿件
AN - SCOPUS:84885981750
SN - 9783642402050
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 328
EP - 333
BT - Algebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013, Proceedings
T2 - 5th International Conference on Algebra and Coalgebra in Computer Science, CALCO 2013
Y2 - 3 September 2013 through 6 September 2013
ER -