Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer (2004)
Bidoit, M., Hennicker, R.: Constructor-based observational logic. J. Log. Algebr. Program. 67(1-2), 3–51 (2006)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude. LNCS, vol. 4350. Springer, Heidelberg (2007)
Futatsugi, K., Găină, D., Ogata, K.: Principles of proof scores in CafeOBJ. Theor. Comput. Sci. 464, 90–112 (2012)
Găină, D., Futatsugi, K.: Initial Semantics in Logics with Constructors. J. Log. Comput. (2013), http://dx.doi.org/10.1093/logcom/exs044
Găină, D., Lucanu, D., Ogata, K., Futatsugi, K.: On Automation of OTS/CafeOBJ method (submitted, 2013)
Găină, D.: Interpolation in logics with constructors. Theor. Comput. Sci. 474, 46–59 (2013)
Găină, D., Futatsugi, K., Ogata, K.: Constructor-based logics. J. UCS 18(16), 2204–2233 (2012)
Hendrix, J.D.: Decision Procedures for Equationally Based Reasoning. Technical Report, UIUC (2008)
Lucanu, D., Goriac, E.-I., Caltais, G., Roşu, G.: CIRC: A Behavioral Verification Tool Based on Circular Coinduction. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 433–442. Springer, Heidelberg (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Găină, D., Zhang, M., Chiba, Y., Arimoto, Y. (2013). Constructor-Based Inductive Theorem Prover. In: Heckel, R., Milius, S. (eds) Algebra and Coalgebra in Computer Science. CALCO 2013. Lecture Notes in Computer Science, vol 8089. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40206-7_26
Download citation
DOI: https://doi.org/10.1007/978-3-642-40206-7_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40205-0
Online ISBN: 978-3-642-40206-7
eBook Packages: Computer ScienceComputer Science (R0)