The Mondex Case study is still the most substantial contribution to the Grand Challenge repository. It has been the target of a number of formal verification efforts. Those efforts concentrated on correctness proofs for refinement steps of the specification in various specification formalisms using different verification tools. In this paper we report on a Java Card implementation of the Mondex protocol and on proving its correctness using the KeY tool. The security properties to be proved are formalised in the Java Modelling Language and follow as closely as possible the concrete layer of the previous Z specification. This work demonstrates that with an appropriate specification language and verification tool, it is possible to bridge the gap between specification and implementation ensuring a fully verified result.

Formal methods can only gain widespread use in industrial software development if they are integrated into software development techniques, tools, and languages that are used in practice. The objective of this tutorial is to show how formal specification and deductive verification of object-oriented programs can be done within a software development platform that supports contemporary design and implementation methodologies. The KeY System (developed by the tutorial presenters) is used for demonstration purposes, which implements our approach and integrates formal methods into the commercial CASE tool Borland Together Control Center 6.2 and, alternatively, the open extensible IDE Eclipse.

We propose an extension of the design-by-contract approach. In addition to preconditions, postconditions, and invariants as the basis for proving properties of a program, information is also provided on which parts of the state are not changed by running the program. This is done in the form of modifier sets. We present a precise semantics of modifier sets and theorems on how to use them in program-correctness proofs. This technique has been implemented as part of the KeY system.

This paper gives a brief description of the KeY system, a tool written as part of the ongoing KeY project 1 , which is aimed at bridging the gap between (a) OO software engineering methods and tools and (b) deductive verification. The KeY system consists of a commercial CASE tool enhanced with functionality for formal specification and deductive verification. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Starting from the textbook formulation of the tableau calculus we give an operational description of the tableau method in terms of abstract state machines at various levels of refinement ending after four stages at a specification that is very close to the lean TAP implementation of the tableau calculus in PROLOG. Proofs of correctness and completeness of the refinement steps are given.

Binary decision diagrams (BDDs) are a well-known tool for representing Boolean functions. We show how BDDs can be extended to full first-order logic by integrating means for representing quantifiers. The resulting structures are called Shannon graphs. A calculus based on these Shannon graphs is set up, and its soundness and completeness proofs are outlined. A comparison of deduction with first-order BDDs and semantic tableaux shows that both calculi are closely related. From a practical perspective, however, BDDs have advantages over tableaux: they provide a more compact representation, since BDDs can be understood as a linear, graphical representation of a fully expanded tableaux. Furthermore, BDDs represent not only the models of a formula, but also its counter-models: this offers a very efficient way to represent lemmata during the proof search. The last part of the paper introduces a compilation-based approach to implementing deduction systems based on Shannon graphs. The idea is to compile the graphs into programs that carry out the proof search at run time.

Abstract We prove the hereditary undecidability of the Lt theories of: (1) torsion-free Hausdorff topological abelian groups; (2) locally pure Hausdorff topological abelian groups.