The KeY tool,10.1007/s10270-004-0058-x,Software and System Modeling,Wolfgang Ahrendt,Thomas Baar,Bernhard Beckert,Richard Bubel,Martin Giese,Reiner Hä

The KeY tool   (Citations: 157)
BibTex | RIS | RefWorks Download
KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal methods and object-oriented development techniques are applied in an integrated manner. Formal specification is performed using the Object Constraint Language (OCL), which is part of the UML standard. KeY provides support for the authoring and formal analysis of OCL constraints. The target language of KeY based development is Java Card DL, a proper subset of Java for smart card applications and embedded systems. KeY uses a dynamic logic for Java Card DL to express proof obligations, and provides a state-of-the-art theorem prover for interactive and automated verification. Apart from its integration into UML based software development, a characteristic feature of KeY is that formal specification and verification can be introduced incrementally.
Journal: Software and System Modeling - SOSYM , vol. 4, no. 1, pp. 32-54, 2005
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...Program verication enables proofs that programs do the right thing, and there has been a lot of work on verifying object-oriented languages, for examples [6, 8, 2, 1]. However, the majority of this work falls short of reasoning about these new features from functional programming such as generics or delegates...
    • ...f list(xs,[1,2,3],Int) list(ys,[4,5,6],Int)g...
    • ...zs = List.appendhIntegeri(xs,ys); f list(zs,[1,2,3,4,5,6],Int)g...
    • ...f m : Math list(x,[1,2,3,4],Int)g d = m.isEven; f list(x,[1,2,3,4],Int) 8 v : Val...
    • ...f m : Math list(x,[1,2,3,4],Int)g d = m.isEven; f list(x,[1,2,3,4],Int) 8 v : Val...
    • ...d7! h(i).fInt(i,v)gfr. Int(i,v) r=even(v)gi g ListhIntegeri.lter(x,d); f list(x,lter([1,2 ,3,4],even),Int) g f list(x,[2,4],Int)g...

    Kasper Svendsenet al. Verifying Generics and Delegates

    • ...out OCL invariants or structural subtyping [2] for models with OCL invariants, which requires that the invariant of a subclassimpliestheinvariantofitssuperclass.Sincesubtype consistency isanimportantrequirementforclassmodels,we refine our definition of consistency as follows...
    • ...The KeY tool, an interactive reasoning environment for UML/OCL that translates constrained models into dynamic logic, is presented in Ahrendt et al. [2]...

    Michael Wahleret al. Efficient analysis of pattern-based constraint specifications

    • ...JACK [2, 6], Why/Krakatoa [12, 20 ]a nd KeY [1, 3] are three available environments for verification of Java programs specified in JML...
    • ...The tool has an easy-to-use graphical interface and seamlessly integrates automated and interactive verification [1, 3]. KeY also uses Simplify...

    Lydie du Bousquetet al. Reusing a JML Specification Dedicated to Verification for Testing, and...

    • ...KeY While the KeY tool was adapted to accept JML, it also supports other languages [1]...

    Patrice Chalinet al. Towards an industrial grade IVE for Java and next generation research ...

    • ...LOOP, KIV, KeY, Jive, and Krakatoa have been used to verify a variety of Java programs [1, 8, 14, 14, 17, 42]...

    Karen Zeeet al. An Integrated Proof Language for Imperative Programs

Sort by: