Bernhard Beckert (firstname.lastname@example.org)
Fri, 9 Nov 2001 16:22:01 +0100 (MET)
Announcement The first prototype of the KeY Tool is now publicly available. It can be downloaded from the KeY web site at http://i12www.ira.uka.de/~key What is KeY? KeY is a joint project of Universitšt Karlsruhe (Germany) and Chalmers University, Gothenburg (Sweden). The KeY system enhances the commercial UML CASE tool Together Control Center with functionality for formal specification and deductive verification. What does KeY aim at? KeY aims at integrating formal specification and verification of software into the software development process. The ultimate goal of the KeY project is to facilitate and promote the use of formal verification as an integral part of the development process of Java Card applications in an industrial context. The main features of KeY: * User continues to work in familiar modeling environment. * Support for parsing and pattern-based generation of OCL constraints. * Dynamic Logic as basis for reasoning about models and implementations. * Target language Java Card. * Integrated automated and interactive proof tools. System Requirements: * The CASE tool Together ControlCenter(tm), Version~5.01 or higher. A free trial version as well as a free academic license are available from TogetherSoft (http://www.togethersoft.com). * Java Runtime Environment (Version~1.3.0 or later). * Linux or Solaris (Windows version in preparation). Contact and Further Information: Email: email@example.com Web site: http://i12www.ira.uka.de/~key KeY Mailing List: If you are interested in the KeY project and would like to get information on future developments, updates, etc., then please become a member of the KeY-Info mailing list. To subscribe send an email to firstname.lastname@example.org with the word "subscribe" in the body of the mail.