- KeY
KeY is a formal software development tool that aims to integrate design, implementation,
formal specification , andformal verification ofobject-oriented software. It supports programs written in Java (more precisely: in a superset ofJava Card ) and specifications written inJML or OCL. At the core of the system is a deductivetheorem prover . It employs a free variablesequent calculus for first-order dynamic logic for Java Card.The development of KeY has been started in autumn 1998 and is an ongoing effort. KeY is jointly developed by the
University of Karlsruhe ,Chalmers University of Technology in Gothenburg, and theUniversity of Koblenz . It is licensed under theGPL .Java Card DL
The theoretical foundation of KeY is a
formal logic called Java Card DL. It is a version of dynamic logic tailored to Java Card programs. As such, it for example allows statements (formulas) like p → [j] q, which intuitively says that q must hold in all program states reachable by executing the Java Card program j in any state that satisfies p. Proofs of the validity of such formulas can then be performed by means of a sequent calculus andsymbolic execution .Other Supported Logics
Besides the core tool based on Java Card DL, there are several variants of KeY which support reasoning for other kinds of logics:
* Dynamic Logic forMISRA C [http://www.cs.ru.nl/~tews/cv07/ifm07.pdf] (KeY-C) (*)
* Differential dynamic logic (dL) [http://www.functologic.com/logic/dL.html] (KeYmaera [http://www.functologic.com/info/KeYmaera.html] , external) (*)
* Logic forAbstract state machines [http://www.inf.ethz.ch/research/disstechreps/theses/show?serial=436&lang=en] (ASMKeY, external)
* A logic forJCSP programs [http://www.cs.chalmers.se/~philipp/publications/jcsp2005.pdf](*) under active development/maintained
Variants of the KeY System
KeY for C
"KeY for C" is an adaption of the KeY System to
MISRA C , a subset of theC programming language .Symbolic Execution Debugger
The "Symbolic Execution Debugger" visualizes the
control flow of a program as asymbolic execution tree that contains all feasible execution paths through the program up to a certain point.The Symbolic Execution Debugger is provided as a plugin to the Eclipse development platform.
KeY-Hoare
"KeY-Hoare" is built on top of KeY and features a
Hoare calculus with state updates. State updates are a means of describing state transitions in aKripke structure .KeYmaera
"KeYmaera" [http://www.functologic.com/info/KeYmaera.html] (previously called HyKeY) is a deductive verification tool for hybrid systems based on a calculus for the differential dynamic logic dL [http://www.functologic.com/logic/dL.html] .It extends the KeY tool with
Mathematica and corresponding algorithms and proof strategies such that it can be used for practical verification ofhybrid systems .KeYmaera has been developed at the
University of Oldenburg .KeY Test Case Generator
KeY is usable as a
model-based testing tool that can generateunit tests for Java programs. The model from which test data and the test case are derived consists of a formal specification (provided inJML or OCL) and a symbolic execution tree of the implementation under test which is computed by the KeY system.Sources
* [http://www.springer.com/east/home/generic/search/results?SGWID=5-40109-22-173712406-0 Verification of Object-Oriented Software: The KeY Approach] . Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt (Eds.). Springer, 2007. ISBN 978-3-540-68977-5.
* [http://i12www.ira.uka.de/%7Ekey/doc/2005/sosym.pdf The KeY Tool] . Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager, and Peter H. Schmitt. Software and Systems Modeling, Springer, 2005.
* [http://cl.cse.wustl.edu/papers/vstte05.pdf Programming With Proofs: Language Based Approaches To Totally Correct Software] . Aaron Stump. Verified Software: Theories, Tools, and Experiments, 2005.
* [http://www.software-kompetenz.de/en/?target=25365 Beispielanwendung KeY] VESK. German only.See also
*
Abstract state machines
*B-Method
* BLAST
*ESC/Java2
* [http://www.informatik.uni-augsburg.de/lehrstuehle/swt/se/kiv/ KIV]
* Spec#External links
* [http://www.key-project.org Home page of the KeY project]
Wikimedia Foundation. 2010.