Specware Logo

Home | Releases | Documentation | Support

Specware is now available on Github at https://github.com/KestrelInstitute/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.

bullet 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

bullet 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

bullet 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

The Specware system consists of a formal specification language, Metaslang, and a variety of support tools. A Metaslang specification is comprised of types, operators, axioms expressed in higher-order logic, and definitions. Specifications are structured using importation and composition by colimit, a category-theoretic universal construction. Metaslang supports higher-order operations and polymorphic types with predicate subtypes.

Specware provides a standard library, specifying basic data types with verified proofs, and executable refinements. It also has built up a library of over 40 transformations for generating refinements.

Specware is self-specified. It has backends to generate executable CommonLisp, C, Java, or Haskell code. It has a translator from Metaslang to Isabelle/HOL that is used to discharge proof obligations.