| Releases | Documentation | Support | Ordering Info
Portions of this site are currently under construction.
Please bear with us; there are new and exciting changes afoot.
Welcome to Specware
What is Specware?
Specware is a software engineering tool that automatically generates
Specware is a leading-edge automated software development system that allows
users to precisely specify the desired functionality of their
applications and to generate provably correct code based on
these requirements. At the core of the design process in Specware lies stepwise
refinement, in which users begin with a simple, abstract model of
their problem and iteratively refine this model until it uniquely and
concretely describes their application.
- a design tool, because it can represent and manipulate designs for
- a (higher order) logic, because it can describe concepts in a formal language with rules of deduction
- a specification language, for expressing functional programs as well as safety and security constraints
- a transformation system and library, for deriving high assurance software
- a database, because it can store and manipulate collections of concepts, facts, and relationships
- be used to develop domain theories
- be used to develop code from specifications, with machine-checkable proofs of correctness
- be used to develop specifications from code
Specware has been used for...
- developing a small operating system
- generating transportation resource schedulers
- generating diverse implementations of the same specification
- generating a family of concurrent garbage collectors