Specification & Formal Analysis of Java Programs
Abstract
Much effort in computer science is readily focused on software adaptation, but it remains an open challenge to adequately predict the behavior of systems subject to adaptation. One approach to solving this problem is the use of formal methods. In this tutorial we show how Java programs can be formally specified using the Java Modeling Language (JML), and how they can be analysed using techniques such as deductive verification and symbolic execution. The KeY System (co-developed by the tutorial presenter) will be used for demonstration purposes. It can be used to formally verify Java programs against specification contracts written in JML, and also to generate test cases with high code coverage. We give a brief introduction into the underlying theoretical concepts (dynamic logic, symbolic execution, contracts, invariants) followed by hands-on exercises with practical analysis tasks. We assume basic familiarity with first-order logic, operational semantics, and object-oriented programming. The KeY system is freely available from the project website and runs on Linux, Mac, and Windows systems that have Java installed.Slides
Note: These all of these slides will actually be used for the tutorial, some are background material- Part 1: Introduction (screen, print)
- Part 2: The Java Modeling Language (screen, print)
- Part 3: Dynamic Logic (screen, print)
- Part 4: Verifying Java Programs (screen, print)
The KeY Tool
The KeY System can be downloaded from the download page at the KeY Project's web site. Please download and install Version 1.4. This can easily be done using Java Web Start (you can start KeY directly from your Web browser). The following test gives an introduction in using the KeY system: keyintro.pdf.Examples
The following zip file contains example KeY input files and proofs: examples.zip
Bernhard Beckert