Summary. Abstract Execution (AE) is a new program analysis technique for automatically proving second-order properties about programs. It is based on the symbolic execution of abstract programs with second-order symbolic stores. Abrupt completion is analyzed in separate SE branches. AE has been successfully applied to show that almost all statement-based Java refactoring techniques are unsound—unless constrained with suitable preconditions. Assuming these preconditions, we automatically proved the transformations correct. With REFINITY, there is now tool support for using AE for your own problems.
Continue reading “Proving the Correctness of Program Transformations with Abstract Execution and REFINITY”
The KeY to Software Correctness
Decades of experience in proving program correctness for Java.
Exception in thread "main" java.lang.ArrayIndexOutOfBoundsException: 40 at java.util.TimSort.pushRun(TimSort.java:413) at java.util.TimSort.sort(TimSort.java:240) at java.util.Arrays.sort(Arrays.java:1438) at TestTimSort.main(TestTimSort.java:18)
The TimSort Success Story
Read about how KeY was used to find a well-concealed bug in the Java standard library.
Functional Verification
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.
Symbolic Debugging
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
Proving Smart Contracts with KeY
With smart contracts, it is really important to get them right at the first try. See how KeY can be used to prove the correctness of Hyperledger Fabric chaincode!
18th KeY Symposium 2019
The KeY Symposium brings together researchers interested in KeY and related aspects. We will exchange recent achievements, current ideas, discuss the next steps and milestones of the area, as well as future directions in general. Also the latest developments in the KeY tool are presented and discussed.
Continue reading “18th KeY Symposium 2019”Functional Verification
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!
Teaching & Research It was never easier to fall in love with formal methods.
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!
