CCC - The CASL Consistency Checker (bibtex)

by Christoph Lüth, Markus Roggenbach and Lutz Schröder

Abstract:

We introduce the CASL Consistency Checker (CCC), a tool that supports consistency proofs in the algebraic specification language CASL. CCC is a faithful implementation of a previously described consistency calculus. Its system architecture combines flexibility with correctness ensured by encapsulation in a type system. CCC offers tactics, tactical combinators, forward and backward proof, and a number of specialised static checkers, as well as a connection to the CASL proof tool HOL-CASL to discharge proof obligations. We demonstrate the viability of CCC by an extended example taken from the CASL standard library of basic datatypes.

View PDF

Reference:

Christoph Lüth, Markus Roggenbach and Lutz Schröder: CCC - The CASL Consistency Checker, In José Fiadeiro, ed.: Recent Trends in Algebraic Development Techniques, 17th International Workshop (WADT 2004), Lecture Notes in Computer Science, vol. 3423, pp. 94–105, Springer; Berlin; http://www.springer.de, 2005. [preprint]

Bibtex Entry:

@InProceedings{LuethEA04,
  author = {Christoph L{\"u}th and Markus Roggenbach and Lutz Schr{\"o}der},
  title = {CCC - The CASL Consistency Checker},
  year = {2005},
  editor = {Jos{\'e} Fiadeiro},
  booktitle = {Recent Trends in Algebraic Development Techniques, 17th International Workshop (WADT 2004)},
  publisher = {Springer; Berlin; http://www.springer.de},
  series = {Lecture Notes in Computer Science},
  volume = {3423},
  pages = {94-105},
  keywords = {Consistency CASL tool support},
  url = {http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=3423&spage=94},
  comment = {<a href="http://www8.informatik.uni-erlangen.de/~schroeder/papers/ccc.ps">[preprint]</a>},
  abstract = {  We introduce the CASL Consistency Checker (CCC), a tool that
  supports consistency proofs in the algebraic specification language
CASL.  CCC is a faithful implementation of a previously described
  consistency calculus. Its system architecture combines flexibility
  with correctness ensured by encapsulation in a type system.  CCC
  offers tactics, tactical combinators, forward and backward proof,
  and a number of specialised static checkers, as well as a connection
  to the CASL proof tool HOL-CASL to discharge proof obligations.
  We demonstrate the viability of CCC by an extended example taken
  from the CASL standard library of basic datatypes.
},
}