Tecton is a language and tool framework whose purpose is to foster structured development of computational systems (both hardware designs and software), using abstraction and specialization as the key structuring mechanisms. Most of the development of Tecton has been conducted jointly with Deepak Kapur and his group at The University at Albany, with support from the National Science Foundation.
D. Kapur, D. R. Musser, and X. Nie, ``The Tecton Proof System,'' Proc. of a Workshop on Formal Methods in Databases and Software Engineering, Concordia University, Montreal, May 15-16, 1992. A much expanded version appeared as ``An Overview of the Tecton Proof System,'' Theoretical Computer Science, Vol. 133, pp. 307-339, October 24, 1994.
D. Kapur and D. R. Musser, Tecton: a framework for specifying and verifying generic system components, invited talk at TPCD Conf. 1992 (Theorem Provers in Circuit Design), University of Nijmegen, The Netherlands, June 22-24, 1992 Rensselaer Polytechnic Institute Computer Science Technical Report 92-20, July, 1992.
D. Kapur and D. R. Musser, Examples of Tecton Concept Descriptions (Working Paper). This paper gives a variety of examples, including an extended example of software specification (generic parallel-reduction and sorting algorithms). However, it offers very little commentary, and there are some known inconsistencies in the style and content of the examples. It is mainly used as a repository of experiments with the Tecton concept description language.
D.R. Musser and Changqing Wang, "A Basis for Formal Specification and Verification of Generic Algorithms in the C++ Standard Template Library", Rensselaer Polytechnic Institute Computer Science Department Technical Report 95-1, January, 1995.
C. Wang and D. R. Musser, "Dynamic Verification of C++ Generic Algorithms," an expanded version of the paper "Dynamic Verification of C++ Generic Components: A Practical Method and Its Support System," November 1995, in Proceedings of Formal Methods in Software Practice Workshop, San Diego, CA, January 10-11, 1996.
Changqing Wang, Integrating Tools and Methods For Rigorous Analysis of C++ Generic Library Components, Ph.D Thesis, Department of Computer Science, Rensselaer Polytechnic Institute, July, 1996.
If you have any questions or comments about any of these papers, please send e-mail to musser@cs.rpi.edu.