The KeYNote series is a virtual workshop where teams from Germany, the Netherlands, Norway and Sweden (in lexicographic order) take part and present recent work which uses or extends the KeY verification system.
Tired of experiencing bugs that weren't covered by your test cases before? KeY lets you augment your Java program with a specification written in the Java Modeling Language JML and helps you proving that your program behaves as it should.
Debugging sucks! Well, not if you're using our Symbolic Execution Debugger. Profit from a graphical visualization of the program's execution flow, state inspection and various other features to quickly uncover undesired behavior!
Teaching and Research
KeY is already used extensively for teaching at different universities. Use the tool's possibilities for teaching your students important concepts like design by contract, applied logics and program verification. Or use KeY for realizing your research project.
Most Recent Posts
Just in time for the holiday season, the new book has arrived.
The LNCS volume 12345* “Deductive Software Verification: Future Perspectives” contains a collection of articles – reflections on the occasion of 20 years of KeY.
The original challenge comes from a real-world situation. There is no particular “trick” needed for the specification and verification; it is rather straightforward. Yet, the required annotations to achieve the specification are not too few – making the example a good opportunity to compare different specification languages. Continue reading “Proving Line Wrapping in KeY, Why3, Dafny and Frama-C”
During the VerifyThis competition 2021, KeY was invited to present itself as a Java verification tool.
It is customary for Verify This that for one tool after a brief introduction into the concepts of the tool, the participants are invited to solve a micro challenge – with a little help from present KeY developers.
After almost 2 years of active development, we present now KeY 2.8 just before the year’s end.
The new KeY version comes with significant improvements on the calculus side, but features also a major overhaul of the user interface.
We thank all contributors for reaching this milestone.
Nice holidays and a happy new year!
The KeY Team
We can do better than testing!
KeY lets you specify the desired behavior of your program in the well-known specification language JML, and helps you proving that your programs conforms to its specification. That way, you did not only show that your program behaves as expected for some set of test values - you proved that it works correctly for all possible values! Go beyond testing - start proving!
Symbolic Debugging The next-generation debugger.
Imagine that you start debugging without having to think of particular input values. Your debugger instantly tells you that part of your code is unreachable, shows you all feasible runs in a beautiful graph and gives you graphical hints on where the problem you're after could possibly hide. While performing all this magic, it gracefully integrates within the Eclipse IDE and offers tools (breakpoints etc.) that you know from the debuggers of yesterday. Meet the Symbolic Execution Debugger!
Use our tool to demonstrate to your students that formal concepts, like first-order logic, Hoare logic and symbolic execution, are not just dry theoretical ideas, but are practically used and even integrated into the IDE they know. KeY is already extensively used in different universities, in several countries.
Currently, our team is spending a lot of effort on making KeY even more attractive to new research projects by increasing its extensibility. Use KeY for your own research project or in your courses!