Welcome to Specware

What is Specware?

Specware is a software engineering tool that automatically generates high-assurance software.

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.

Specware is...

• a design tool, because it can represent and manipulate designs for complex systems
• 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

Specware can...

• 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