Specware Overview

Specware is a next-generation environment supporting the design, development and automated synthesis of scalable, correct-by-construction software. It represents the confluence of capabilities and lessons learned from our earlier prototype systems (KIDS, REACTO, DTRE), grounded on a strong mathematical foundation (SLANG, based on category theory). The current version of Specware is a robust implementation of this foundation. We anticipate that many colleagues will add to the theory/specification library. We also anticipate the development of new front-ends to help put these software specification and synthesis capabilities into the hands of a wider group of end-users. Specware supports automation of

• component-based specification of programs using a graphical interface
• incremental refinement of specifications into correct code in various target languages (e.g. C++, LISP, Ada, Cobol)
• design and synthesis of software architectures/frameworks
• design and synthesis of algorithm schemas
• design and synthesis of reactive systems
• data-type refinement
• program optimization
• recording and experimenting with different design decisions
• domain-knowledge capture, verification and manipulation

Click here to go to Kestrel's Home Page