Constructor-based inductive theorem prover

Daniel Gǎinǎ, Min Zhang, Yuki Chiba, Yasuhito Arimoto

Research output: Chapter in Book/Report/Conference proceedingConference contribution

18 Citations (Scopus)


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.

Original languageEnglish
Title of host publicationAlgebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013, Proceedings
Number of pages6
Publication statusPublished - Oct 28 2013
Externally publishedYes
Event5th International Conference on Algebra and Coalgebra in Computer Science, CALCO 2013 - Warsaw, Poland
Duration: Sept 3 2013Sept 6 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8089 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other5th International Conference on Algebra and Coalgebra in Computer Science, CALCO 2013

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Constructor-based inductive theorem prover'. Together they form a unique fingerprint.

Cite this