Constructor-based inductive theorem prover

Daniel Mircea Gaina, Min Zhang, Yuki Chiba, Yasuhito Arimoto

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

11 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationAlgebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013, Proceedings
Pages328-333
Number of pages6
DOIs
Publication statusPublished - Oct 28 2013
Externally publishedYes
Event5th International Conference on Algebra and Coalgebra in Computer Science, CALCO 2013 - Warsaw, Poland
Duration: Sep 3 2013Sep 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

Other

Other5th International Conference on Algebra and Coalgebra in Computer Science, CALCO 2013
CountryPoland
CityWarsaw
Period9/3/139/6/13

Fingerprint

Theorem
Software System
Logic
Strategy

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Gaina, D. M., Zhang, M., Chiba, Y., & Arimoto, Y. (2013). Constructor-based inductive theorem prover. In Algebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013, Proceedings (pp. 328-333). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8089 LNCS). https://doi.org/10.1007/978-3-642-40206-7-26

Constructor-based inductive theorem prover. / Gaina, Daniel Mircea; Zhang, Min; Chiba, Yuki; Arimoto, Yasuhito.

Algebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013, Proceedings. 2013. p. 328-333 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8089 LNCS).

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

Gaina, DM, Zhang, M, Chiba, Y & Arimoto, Y 2013, Constructor-based inductive theorem prover. in Algebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8089 LNCS, pp. 328-333, 5th International Conference on Algebra and Coalgebra in Computer Science, CALCO 2013, Warsaw, Poland, 9/3/13. https://doi.org/10.1007/978-3-642-40206-7-26
Gaina DM, Zhang M, Chiba Y, Arimoto Y. Constructor-based inductive theorem prover. In Algebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013, Proceedings. 2013. p. 328-333. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-40206-7-26
Gaina, Daniel Mircea ; Zhang, Min ; Chiba, Yuki ; Arimoto, Yasuhito. / Constructor-based inductive theorem prover. Algebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013, Proceedings. 2013. pp. 328-333 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{0b4803f3a8de4d3da3daf7e130738255,
title = "Constructor-based inductive theorem prover",
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.",
author = "Gaina, {Daniel Mircea} and Min Zhang and Yuki Chiba and Yasuhito Arimoto",
year = "2013",
month = "10",
day = "28",
doi = "10.1007/978-3-642-40206-7-26",
language = "English",
isbn = "9783642402050",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "328--333",
booktitle = "Algebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013, Proceedings",

}

TY - GEN

T1 - Constructor-based inductive theorem prover

AU - Gaina, Daniel Mircea

AU - Zhang, Min

AU - Chiba, Yuki

AU - Arimoto, Yasuhito

PY - 2013/10/28

Y1 - 2013/10/28

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 - http://www.scopus.com/inward/record.url?scp=84885981750&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84885981750&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-40206-7-26

DO - 10.1007/978-3-642-40206-7-26

M3 - Conference contribution

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

ER -