KeY: Difference between revisions
added list of supported logics |
No edit summary |
||
| Line 1: | Line 1: | ||
{{notability|date=July 2007}} |
{{notability|date=July 2007}} |
||
'''KeY''' is a formal software development tool that aims to integrate design, implementation, |
'''KeY''' is a formal software development tool that aims to integrate design, implementation, |
||
[[formal specification]], and [[formal verification]] of [[object-oriented]] software. It supports programs written in [[Java (programming language)|Java]] ( |
[[formal specification]], and [[formal verification]] of [[object-oriented]] software. It supports programs written in [[Java (programming language)|Java]] (more precisely: in a superset of [[Java Card]]) and specifications written in [[JML]] or [[Object Constraint Language|OCL]]. At the core of the system is a deductive [[theorem prover]]. It employs a free variable [[sequent calculus]] for first-order [[dynamic logic (modal logic)|dynamic logic]] for Java. |
||
KeY is jointly developed by the [[University of Karlsruhe]], [[Chalmers University of Technology]] in Gothenburg, and the [[University of Koblenz]]. |
KeY is jointly developed by the [[University of Karlsruhe]], [[Chalmers University of Technology]] in Gothenburg, and the [[University of Koblenz]]. |
||
Revision as of 19:16, 31 July 2007
 | The topic of this article may not meet Wikipedia's general notability guideline. (July 2007) |
KeY is a formal software development tool that aims to integrate design, implementation, formal specification, and formal verification of object-oriented software. It supports programs written in Java (more precisely: in a superset of Java Card) and specifications written in JML or OCL. At the core of the system is a deductive theorem prover. It employs a free variable sequent calculus for first-order dynamic logic for Java.
KeY is jointly developed by the University of Karlsruhe, Chalmers University of Technology in Gothenburg, and the University of Koblenz.
Supported Logics
The KeY tool (resp. external maintained variants) support reasoning for several kinds of logics:
- JavaCardDL (main logic supported by the core tool) (*)
- Dynamic Logic for MisraC [1] (extension) (*)
- Differential dynamic logic (dL) [2] (HyKeY [3], external) (*)
- Logic for Abstract state machines [4] (ASMKeY, external)
- A logic for JCSP programs [5]
(*) under active development/maintained
Sources
- 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.
- 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.
- Programming With Proofs: Language Based Approaches To Totally Correct Software. Aaron Stump. Verified Software: Theories, Tools, and Experiments, 2005.
See also
External links
 | This computer science article is a stub. You can help Wikipedia by expanding it. |