Home | Releases | Documentation | Support | Ordering Info
- User Manual(view .pdf)
The User Manual serves as a guide to Specware usage.
The Tutorial will guide you through the process of specifying, refining and generating code in
Specware. A comprehensive example provides step-by-step instructions for this development process (Under Construction).
- Language Manual (view .pdf)
The Language Manual gives a comprehensive treatment of all Specware language constructs.
- Isabelle Interface Manual (view .pdf)
The Specware to Isabelle Interface Manual documents how to use Isabelle/HOL to discharge Specware proof obligations.
- Quick Reference Guide (View .pdf)
The Quick Reference guide is a brief 2-page summary of Specware shell commands and language constructs.
- Specware Transformation Manual
The Specware Transformation Manual is a brief guide to Specware's transformation script language and the interaction shell for building transformation scripts (Under Construction).
See the ordering page for more information about getting Specware.
Network Vulnerability Analysis - A Formal Approach. James McDonald and John Anton. March 2001.
SPECWARE - Producing Software Correct by Construction. James McDonald and John Anton. March 2001.
The Architecture of Specware, a Formal Software Development System. Yellamraju V. Srinivas and James L. McDonald Kestrel Institute Technical Report KES.U.96.7, August 1996.
Mechanizing the Development of Software D. R. Smith. Calculational System Design, Proceedings of the International Summer School Marktoberdorf, M. Broy (Ed.), NATO ASI Series, IOS Press, Amsterdam, 1999. Kestrel Institute Technical Report KES.U.99.1, March 1999.
Planware -- Domain-Specific Synthesis of High-Performance Schedulers. Lee Blaine, Li-Mei Gilham, Junbo Liu, Douglas R. Smith, and Stephen Westfold. Proceedings of the Thirteenth Automated Software Engineering Conference, IEEE Computer Society Press, Los Alamitos, CA, October 1998, pp. 270-280. Kestrel Institute Technical Report KES.U.98.6, September 1998.
Specware®: Formal Support for Composing Software. Y. V. Srinivas and Richard Jullig, Proceedings of the Conference on Mathematics of Program Construction, Kloster Irsee, Germany, July 1995. Kestrel Institute Technical Report KES.U.94.5.
Specware® Language Manual 2.0.1. Richard Waldinger, et al. Suresoft, Inc., 1996.
Towards a Provably-Correct Implementation of the JVM Bytecode Verifier. Alessandro Coglio, Allen Goldberg, and Zhenyu Qian. Proceedings of the OOPSLA '98 Workshop on the Formal Underpinnings of Java, Vancouver, B.C., October 1998. Kestrel Institute Technical Report KES.U.98.5, August 1998.
Producing More Reliable Software: Mature Software: Engineering Process vs. State-of-the-Art Technology. Widmaier, J, C. Smidts, and X. Huang. University of Maryland Reliability Engineering Program, 2000.
Creating High Confidence in a Separation Kernel. Abstract.
W.B. Martin, P.D. White, and F.S. Taylor. Automated
Software Engineering, Vol. 9 no. 3, August 2002, pp. 263-284.
Systems Synthesis: Towards a new paradigm and discipline for knowledge, software, and system development and maintenance. Keith Williamson. Mathematics and Computing
Technolgy, Boeing Phantom Works, March 2001.
Industrial Applications of Software Synthesis via Category Theory - Case Studies Using Specware. Williamson, K. et. al. Journal of Automated Software Engineering, Kluwer Academic Publishers, 2001.
Reuse of Knowledge at an Appropriate Level of Abstraction. Williamson, K. et. al. Case Studies Using
Specware, Springer Lecture Notes in Computer Science #1844, International Conference on Software Reuse, 2000.
Applying Category Theory to Derive Engineering Software from Encoded
M. Healy and K. Williamson. (Invited Paper). In, T. Rus, ed., Algebraic Methodology and Software Technology, 8th International
Conference, AMAST 2000, Iowa City, Iowa, USA, May 2000, Proceedings. Lecture Notes
in Computer Science #1816, Springer-Verlag: New York. pp. 484-498.
Deriving Engineering Software from Requirements. Williamson, K. and Healy, M. Journal of Intelligent Manufacturing, Kluwer Academic Publishers, 2000.