Publications

 

This page contains a chronological list of journal and conference papers as well as other documents that are related to the KeY project.

INDEX: Most Important 2012 2011 2010 2009 2008 2007 2006 2005 2004 2003 Older Publications

Most Important

This book is the definitive source for all information related to the KeY project

Verification of Object-Oriented Software: The KeY Approach Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt (Eds.) 15 chapters and 2 appendices, xxix + 658 pages ISBN: 3-540-68977-X Springer-Verlag, LNCS 4334 - BibTeX - Book Website

This paper is (apart from the above book) the best source of information on the KeY project and the KeY tool.

The KeY Tool
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager, and Peter H. Schmitt
Software and Systems Modeling, Springer 2005
Abstract - Springer Online - PDF (preprint) - BibTeX

2012

Semantics of Model Fields in Annotation-based Specifications
Bernhard Beckert and Daniel Bruns
KI 2012: Advances in Artificial Intelligence, Saarbrücken, Germany, 2012.
BibTeX - PDF

 

Model Generation for Quantified Formulas with Application to Test Data Generation
Christoph Gladisch
International Journal on Software Tools for Technology Transfer (STTT)
Abstract - BibTeX - PDF

 

Dynamic trace logic: Definition and proofs
Bernhard Beckert and Daniel Bruns
Technical Report 2012-10, Department of Informatics, Karlsruhe Institute of Technology
BibTeX - PDF

 

The KeY approach for the cryptographic verification of Java programs: A case study
Bernhard Beckert, Daniel Bruns, Ralf Küsters, Christoph Scheben, Peter H. Schmitt, and Tomasz Truderung
Technical Report 2012-8, Department of Informatics, Karlsruhe Institute of Technology
BibTeX - PDF

 

A Proof Assistant for Alloy Specifications
Mattias Ulbrich, Ulrich Geilmann, Aboubakr Achraf El Ghazi, Mana Taghdiri
18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2012
BibTeX - PDF - Technical Report

2011

Verification-based Software-fault Detection
Christoph Gladisch
PhD thesis, Karlsruhe Institute of Technology
PDF - BibTeX

 

Predicate Abstraction in a Program Logic Calculus
Benjamin Weiß
Science of Computer Programming
PDF (preprint) - BibTeX

 

Deductive Verification of Object-Oriented Software: Dynamic Frames, Dynamic Logic and Predicate Abstraction
Benjamin Weiß
PhD thesis, Karlsruhe Institute of Technology
PDF - BibTeX

 

Specification of red-black trees: Showcasing dynamic frames, model fields and sequences (extended abstract)
Daniel Bruns
10th KeY symposium, Nijmegen, The Netherlands, August 2011
PDF - BibTeX - Abstract

 

Formal semantics of model fields inspired by a generalization of Hilbert's ɛ terms (extended abstract)
Bernhard Beckert and Daniel Bruns
10th KeY symposium, Nijmegen, The Netherlands, August 2011
PDF - BibTeX - Abstract

 

Dynamic Frames in Java Dynamic Logic
Peter H. Schmitt, Mattias Ulbrich, Benjamin Weiß
International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), Paris, France, June 2010
PDF - BibTeX - Technical Report

 

Verified Resource Guarantees using COSTA and KeY
Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hähnle, Germán Puebla, and Guillermo Román-Díez
International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), Paris, France, June 2010
PDF

 

Verification of software product lines with delta-oriented slicing
Daniel Bruns, Vladimir Klebanov, and Ina Schaefer
International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), Paris, France, June 2010
PDF - BibTeX - Abstract

 

2010

Visual Interactive Debugger Based on Symbolic Execution
Reiner Hähnle, Markus Baum, Richard Bubel, and Marcel Rothe
25th IEEE/ACM International Conference on Automated Software Engineering (Antwerp, Belgium), ASE 2010
PDF

 

Specifying Imperative ML-like Programs Using Dynamic Logic
Séverine Maingaud and Vincent Balat, Richard Bubel, Reiner Hähnle and Alexandre Miquel
Proc. International Conference on Formal Verification of Object-Oriented Software (FoVeOOS), Paris, France, Springer-Verlag LNCS, FoVeOOS 2010
PDF

 

Verification of Variable Software: an Experience Report
Richard Bubel, Crystal Din, and Reiner Hähnle
Pre-proceedings. International Conference on Formal Verification of Object-Oriented Software (FoVeOOS), Paris, France, FoVeOOS 2010
PDF

 

Interleaving Symbolic Execution and Partial Evaluation
Richard Bubel, Reiner Hähnle and Ran Ji
In Post Conf. Proceedings 7th Intl. Symposium on Formal Methods for Components and Objects, Eindhoven, Netherlands, Springer-Verlag LNCS 6286
PDF (preprint)

 

A System for Compositional Verification of Asynchronous Objects
Wolfgang Ahrendt, Maximilian Dylla
In Science of Computer Programming, Elsevier, 2010
PDF - BibTeX - Abstract

 

A Verification System for Distributed Objects with Asynchronous Method Calls
Wolfgang Ahrendt, Maximilian Dylla
In Formal Methods and Software Engineering, International Conference on Formal Engineering Methods, ICFEM'09, Rio de Janeiro, Brazil, December 2009, Springer, LNCS 5885
PDF - BibTeX - Abstract

 

Test Data Generation For Programs with Quantified First-order Logic Specifications
Christoph Gladisch
In Proceedings of the 22nd IFIP International Conference on Testing Software and Systems, November, 2010, Natal, Brazil
PDF - BibTex - Abstract

 

Generating Regression Unit Tests using a Combination of Verification and Capture & Replay
Christoph Gladisch, Shmuel Tyszberowicz, Bernhard Beckert, Amiram Yehudai
In proceedings of The 4th International Conference on Tests And Proofs (TAP 2010), Malaga, Spain
PDF - BibTeX - Abstract

 

Satisfiability Solving and Model Generation for Quantified First-order Logic Formulas
Christoph Gladisch
International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), Paris, France, June 2010
PDF - BibTeX - Abstract

 

Formal Semantics for the Java Modeling Language (Extended Abstract)
Daniel Bruns
Informatiktage 2010, Bonn, Germany, March 2010
PDF - BibTeX - Abstract

2009

Integrated and Tool-Supported Teaching of Testing, Debugging, and Verification
Wolfgang Ahrendt, Richard Bubel, Reiner Hähnle
In proceedings of the Second International Conference on Teaching Formal Methods
PDF - BibTeX

 

Abstract Interpretation of Symbolic Execution with Explicit State Updates
Richard Bubel, Reiner Hähnle, Benjamin Weiß
In Post Conference Proceedings of the 6th International Symposium on Formal Methods for Components and Objects (FMCO 2008)
PDF - BibTeX

 

Could we have chosen a better Loop Invariant or Method Contract?
Christoph Gladisch
In proceedings of The Third International Conference on Tests And Proofs (TAP 2009), Zürich, Switzerland
PDF - BibTeX

 

Special Issue on Tests and Proofs
Bernhard Beckert, Reiner Hähnle (eds.)
Journal of Automated Reasoning
Springer-Verlag, JAR - BibTeX

 

Verification of Modifies Clauses in Dynamic Logic with Non-rigid Functions
Christian Engel, Andreas Roth, Peter H. Schmitt, Benjamin Weiß
Technical Report 2009-9, Department of Computer Science, University of Karlsruhe
PDF - BibTeX

 

Predicate Abstraction in a Program Logic Calculus
Benjamin Weiß
7th International Conference on integrated Formal Methods (iFM 2009)
PDF - BibTeX

 

2008

Verification-based Testing for Full Feasible Branch Coverage
Christoph Gladisch
6th IEEE Int. Conf. Software Engineering and Formal Methods (SEFM'08)
PDF (preliminary version) - BibTeX - Abstract

 

Specification Predicates with Explicit Dependency Information
Richard Bubel, Reiner Hähnle, Peter H. Schmitt
Proceedings of the 5th International Verification Workshop
PDF - BibTeX

 

Tests and Proofs
Bernhard Beckert, Reiner Hähnle (eds.)
Proceedings of the Second International Conference
BibTeX - Conference Website

 

Tests and Proofs
Bernhard Beckert, Reiner Hähnle (eds.)
Papers presented at the Second International Conference that were not included in the main proceedings
PDF - BibTeX - Abstract - Conference Website

 

Integrating Verification and Testing of Object-Oriented Software
Christian Engel, Christoph Gladisch, Vladimir Klebanov, Philipp Rümmer
In proceedings of the Second International Conference on Tests and Proofs
PDF - BibTeX - Abstract

 

Verification-based Test Case Generation with Loop Invariants and Method Specifications
Christoph Gladisch
In Tests and Proofs: Papers Presented at the Second International Conference, TAP 2008, Italy
BibTeX - Abstract

 

2007

This paper describes the calculus for verifying concurrent Java programs, which has been implemented in the KeY system.

A Dynamic Logic for Deductive Verification of Concurrent Programs
Bernhard Beckert, Vladimir Klebanov
Proceedings, 5th IEEE International Conference on Software Engineering and Formal Methods
PDF (preliminary version) - BibTeX - Abstract

 

A general tutorial paper on specification and verification with the KeY tool.

Verifying Object-Oriented Programs with KeY: A Tutorial
Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Philipp Rümmer, Peter H. Schmitt
5th International Symposium on Formal Methods for Components and Objects, Amsterdam, The Netherlands, November 2006, LNCS 4709, Springer-Verlag
PDF (preliminary version) - BibTeX - Abstract - Example of the paper - Talk

 

In this paper, we discuss how Java Dynamic logic can be used to search for counterexamples that reveal program incorrectness.

Proving Programs Incorrect using a Sequent Calculus for Java Dynamic Logic
Philipp Rümmer, Muhammad Ali Shah
Testing and Proofs, Zurich, February 2007, LNCS 4454, Springer
Abstract - BibTeX - PDF

 

This paper reports the result of our work on the Mondex Card case study. It describes a Java Card implementation of the Mondex protocol, refines the Z specification to a JML specification and proves that the progam satisfies them with the KeY system.

Verifying the Mondex Case Study
Peter H. Schmitt, Isabel Tonin
Software Engineering and Formal Methods (SEFM), London, September 2007, IEEE Press, pp. 47 -- 56.
Abstract - BibTeX - PDF (preliminary version)

 

This paper proposes to use deductive program verification systems to generate specifications for given programs and to then use these specifications as input for black-box testing tools.

White-box Testing by Combining Deduction-based Specification Extraction and Black-box Testing
Bernhard Beckert, Christoph Gladisch
Testing and Proofs, Zurich, February 2007, LNCS 4454, Springer
Abstract - BibTeX - PDF

 

We present a new automatic test generation method for Java Card based on attempts at formal verification of the implementation under test.

Generating Unit Tests from Formal Proofs
Christian Engel, Reiner Hähnle
Testing and Proofs, Zurich, February 2007, LNCS 4454, Springer
PDF (preprint) - BibTeX

 

A paper describing the Java Card API case study.

Fully Verified Java Card API Reference Implementation
Wojciech Mostowski
Verify'07 Workshop at CADE21, Bremen, Germany, July 2007, CEUR Workshop Proceedings
PDF - BibTeX - Verify'07

 

This technical report describes the KeY approach to the well-known Mondex case study.

Verifying the Mondex Case Study.The KeY Approach
Isabel Tonin
Technical Report 2007-4, Universität Karlsruhe
PDF - BibTeX

 

This paper presents an approach for inferring loop invariants using a symbolic execution calculus.

Inferring Invariants by Symbolic Execution
Peter H. Schmitt, Benjamin Weiß
Verify'07 Workshop at CADE21, Bremen, Germany, July 2007, CEUR Workshop Proceedings
PDF - BibTeX - Verify'07

 

A recent overview paper on the architecture and philosophy of the KeY tool (Invited Paper).

KeY: A Formal Method for Object-Oriented Systems
Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt
9th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS), Paphos, Cyprus, June 2007, Springer LNCS 4468, pp 32-43
PDF (preliminary version) - BibTeX - Abstract - Springer LNCS Online

 

A system abstract describing the KeY system's deduction component.

The KeY System (Deduction Component)
Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, and Peter H. Schmitt
International Conference on Automated Deduction (CADE), Bremen, Germany, July 2007, LNCS 4603, pp379-384, Springer
Abstract - BibTeX - PDF

 

A system abstract describing a new instance of the KeY system that supports a fragment of C as its target language.

A Tool for Verification of C Programs
Oleg Mürk, Daniel Larsson, and Reiner Hähnle
International Conference on Automated Deduction (CADE), Bremen, Germany, July 2007, LNCS 4603, pp385-390, Springer
BibTeX - PDF

 

In this paper we show that a flow-sensitive type system ensuring non-interference in a simple while language can be expressed through specialised rules of a program logic.

Integration of a Security Type System into a Program Logic
Reiner Hähnle, Jing Pan, Philipp Rümmer, Dennis Walter
2nd Symposium on Trustworthy Global Computing (TGC), Lucca, Italy, 2006, LNCS 4661, pp 116-131 Springer
PDF (preprint) - BibTeX

 

2006

This publication was produced within the European project HIJA, where KeY was used as the verification tool.

A Case Study of Specification and Verification using JML in an Avionics Application
James J. Hunt, Eric Jenn, Stéphane Leriche, Peter Schmitt, Isabel Tonin, Claus Wonnemann
4th Workshop on Java Technologies for Real-time and Embedded Systems - JTRES 2006
Abstract - BibTeX - PDF (preprint) - ACM Digital Library

 

This publication was produced within the European project HIJA, where KeY was used as the verification tool.

Provably Correct Loops Bounds for Realtime Java Programs
James J. Hunt, Peter H. Schmitt, Fridtjof B. Siebert, Isabel Tonin
4th Workshop on Java Technologies for Real-time and Embedded Systems - JTRES 2006
Abstract - BibTeX - PDF (preprint) - ACM Digital Library

 

Trends and Controversies Department of IEEE Intelligent Systems.

Intelligent Systems and Formal Methods in Software Engineering
Bernhard Beckert, Tony Hoare, Reiner Hähnle, Douglas R. Smith, Cordell Green, Silvio Ranise, Cesare Tinelli, Thomas Ball and Sriram K. Rajamani
IEEE Intelligent Systems
Abstract - BibTeX - IEEE Intelligent Systems

 

An account on the update language that is used in KeY to represent memory.

Sequential, Parallel, and Quantified Updates of First-Order Structures
Philipp Rümmer
13th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Phnom Penh, Cambodia, 2006, LNCS, Springer
Abstract - PDF (preprint) - BibTeX

 

We show that one can replace interactive proof techniques, such as induction, with automated first-order reasoning in order to deal with parallelizable loops.

Automating Verification of Loops by Parallelization
Tobias Gedell, Reiner Hähnle
13th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Phnom Penh, Cambodia, 2006, LNCS, Springer
PDF (preprint) - Springer Link - BibTeX

 

This paper presents a methodology for the formalization of human-computer interaction under security aspects.

A Method for Formalizing, Analyzing, and Verifying Secure User Interfaces
Bernhard Beckert, Gerd Beuster
International Conference on Formal Engineering Methods, Macao, October/November 2006, LNCS, Springer
Abstract - BibTeX - PDF

 

A discussion paper.

Must Program Verification Systems and Calculi be Verified?
Bernhard Beckert, Vladimir Klebanov
VERIFY 2006, Workshop at the International Joint Conference on Automated Reasoning, Seattle, USA
PDF - Abstract - BibTeX

 

This paper describes the formalisation of Java Card special "non-atomic" methods (arrayCopyNonAtomic, arrayFillNonAtomic) in Java Card Dynamic Logic. The paper also contains a brief high level description of how the Java Card transaction mechanism is treated in KeY.

Formal Reasoning about Non-Atomic Java Card Methods in Dynamic Logic
Wojciech Mostowski
Formal Methods (FM) 2006, Hamilton, Ontario, Canada, August 2006, LNCS, Springer.
Abstract - BibTeX - PDF (preprint)

 

This paper introduces the dynamic logic ODL that is enriched with non-rigid functions, and presents a sound and complete calculus for that logic. ODL corresponds to the core of the dynamic logic used in the KeY system.

Dynamic Logic with Non-rigid Functions: A Basis for Object-oriented Program Verification
Bernhard Beckert, Andre Platzer
International Joint Conference on Automated Reasoning, Seattle, USA, August 2006, LNCS, Springer
Abstract - BibTeX - PDF

 

2005

An important subset of Java Dynamic Logic calculus are program transformation rules. This paper discusses our approach to validate these rules against a Maude rewriting semantics of Java.

Automatic Validation of Transformation Rules for Java Verification against a Rewriting Semantics
Wolfgang Ahrendt, Andreas Roth, and Ralf Sasse
12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR, Montego Bay, Jamaica, December 2005, LNCS 3835, Springer
Abstract - PDF (preprint) - BibTeX - Springer Online - Further Material

 

In this paper we give an overview of the different ways in which second-order principles can be expressed in specification languages and logics.

Second-Order Principles in Specification Languages for Object-Oriented Programs
Bernhard Beckert, Kerry Trentelman
12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR, Montego Bay, Jamaica, December 2005, LNCS 3835, Springer
BibTeX - Abstract - Springer Online

 

In this paper we present an improved proof rule for handling while loops in deductive program verification making use of information given in modifier sets.

An Improved Rule for While Loops in Deductive Program Verification
Bernhard Beckert, Steffen Schlager, and Peter H. Schmitt
7th International Conference on Formal Engineering Methods, Manchester, UK
Abstract - PDF (preprint) -

 

In this paper we present an approach to the deductive verification of concurrent Java programs that are implemented using the JCSP library.

Verification of JCSP Programs
Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, and Peter H. Schmitt
Communicating Process Architectures (CPA) 2005, "Concurrent Systems Engineering" series of IOS Press
Abstract - PDF (preprint) - BibTeX

 

This paper describes the (retrenchment) relation between programming language data types and specification language data types.

Refinement and Retrenchment for Programming Language Data Types
Bernhard Beckert and Steffen Schlager
"Formal Aspects of Computing"
Abstract - PDF (preprint)

 

Describes how generated OCL constraints can be automatically simplified.

Simplifying Transformations of OCL Constraints
Martin Giese and Daniel Larsson
Proceedings, International Conference on Model Driven Engineering Languages and Systems (MoDELS), Montego Bay, Jamaica, October 2005.
Abstract - PDF - BibTeX

 

This paper is an abstract description of the part of the KeY calculus that deals with subtyping, type casts, instanceof, etc.

A Calculus for Type Predicates and Type Coercion
Martin Giese
Proceedings, International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Koblenz, Germany, September 2005.
Abstract - PDF - BibTeX

 

Proceedings of the 3rd IEEE International Conference

Software Engineering and Formal Methods
Bernhard Aichernig and Bernhard Beckert (eds.)
BibTeX - Abstract

 

In this paper we develop a method for automatic construction of customised induction rules for proving total correctness of loops in a semi-interactive theorem prover.

Customised Induction Rules for Proving Correctness of Imperative Programs
Ola Olsson and Angela Wallenburg
In proceedings of Software Engineering and Formal Methods, 3rd IEEE International Conference, SEFM 2005, Koblenz, Germany, September 7-9, 2005, IEEE Computer Society Press
Abstract - PDF - BibTeX

Proceedings of the International Conference

Automated Reasoning with Analytic Tableaux and Related Methods
Bernhard Beckert (ed.)
BibTeX - Abstract - Springer Verlag, LNCS 3702

 

This paper describes a technique for embedding static analysis in tableaux and sequent based frameworks.

Embedding Static Analysis into Tableaux and Sequent based Frameworks
Tobias Gedell
14th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Springer LNCS 3702
Abstract - PDF - BibTeX - Springer Verlag, LNCS 3702

 

This paper presents and discusses an approach for proving formulas in Java Dynamic Logic invalid by searching for counterexamples.

Generating Counterexamples for Java Dynamic Logic
Philipp Rümmer
Preliminary Proceedings of Workshop on Disproving at CADE 20, 2005
Abstract - Postscript (preprint) - BibTeX

 

This paper discusses the pros and cons of using many-valued logic for modeling the semantics of partial functions in specification languages.

Many-Valued Logic, Partiality, and Abstraction in Formal Specification Languages
Reiner Hähnle
Logic Journal of the IGPL, Oxford University Press, July 2005
Abstract - PDF (preprint) - BibTeX

 

This paper describes a general program logic approach for the analysis of secure information flow. It supersedes the WITS paper

A Theorem Proving Approach to Analysis of Secure Information Flow
Adam Darvas and Reiner Hähnle and Dave Sands
Proc. 2nd International Conference on Security in Pervasive Computing, SPC'05, Boppard, Germany, Springer-Verlag, 2005
Abstract - PDF (preprint) - BibTeX

 

This paper reports on how encapsulation properties of object-oriented programs can be specified.

Specification and Verification of Encapsulation in Java Programs
Andreas Roth
Formal Methods for Open Object-Based Distributed Systems 2005, Athens, Greece, June 2005, LNCS, Springer.
Abstract - Springer Online - PDF (preprint) - BibTeX

 

This paper describes a system for automatically translating formal OCL specifications to natural language, and the results of using the system on a case study of existing OCL specifications.

Translating Formal Software Specifications to Natural Language — A Grammar-Based Approach
David A. Burke and Kristofer Johannisson
Logical Aspects of Computational Linguistics (LACL 2005), Bordeaux, France, April 2005, LNAI, Springer.
Abstract - Springer Online - PDF (preprint) - BibTeX

This paper reports on the experience with formalising and verifying Java Card security properties from the SecSafe Project. It is based on two case studies: the RSA based authentication applet (SafeApplet) and Demoney. A conference version of the technical report below.

Formalisation and Verification of Java Card Security Properties in Dynamic Logic
Wojciech Mostowski
Fundamental Approaches to Software Engineering Conference (FASE 2005), Edinburgh, Scotland, April 2005, LNCS, Springer.
Abstract - Springer Online - PDF (preprint) - BibTeX

 

This paper describes the first practical experiments involving the throughout modality and transactions.

Verification of Safety Properties in the Presence of Transactions
Reiner Hähnle and Wojciech Mostowski
Proceedings, Construction and Analysis of Safe, Secure and Interoperable Smart devices (CASSIS'04) Workshop, Springer, 2005.
Abstract - Springer Online - PDF (preprint) - BibTeX

 

This paper is right now the best source of information on the KeY project and the KeY tool.

The KeY Tool
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager, and Peter H. Schmitt
Software and Systems Modeling, Springer 2005
Abstract - Springer Online - PDF (preprint) - BibTeX

This paper is the journal version of the FMICS paper and describes a case study of an object-oriented safety critical software.

Integration of Informal and Formal Development of Object-Oriented Safety-Critical Software - A Case Study with the KeY System
Reiner Hähnle and Richard Bubel
International Journal on Software Tools for Technology Transfer (STTT), Springer, 2005
Abstract - PDF (preprint) - BibTeX

 

2004

This rechnical report presents an implementation of a logic for ASM (Abstract State Machines) in the KeY system together with a small case study

The ASMKeY Theorem Prover
Stanislas Nanchen and Hubert Schmid and Peter H. Schmitt and Robert Stärk
BibTeX - Abstract - PDF

 

This paper presents the graphical user interface of the KeY prover. It also explains the role of taclets in the KeY prover from a user interface perspective. For a more technical account, see the `Taclets: A New Paradigm...' paper mentioned further down.

Taclets and the KeY Prover
Martin Giese
Proc. User Interfaces for Theorem Provers Workshop, UITP 2003,
Published 2004 in ENTCS volume 103
Abstract - PDF of free version - BibTeX

 

This master thesis is the long version of the ODL paper at the IJCAR 2006. It introduces the dynamic logic ODL that is enriched with non-rigid functions, and presents a sound and complete calculus for that logic. ODL corresponds to the core of the dynamic logic used in the KeY system.

An Object-oriented Dynamic Logic with Updates
Andre Platzer
Master Thesis at the Universität Karlsruhe, 2004
PDF - BibTeX

 

This paper reports on the experience with formalising and verifying Java Card security properties from the SecSafe Project. It is based on two case studies: the RSA based authentication applet (SafeApplet) and Demoney.

Formalisation and Verification of Java Card Security Properties in Dynamic Logic
Wojciech Mostowski
Chalmers University of Technology, Department of Computing Science, Technical Report 2004-08. Extended version of the FASE'05 paper.
Abstract - PDF - BibTeX

 

This paper describes the Taclet paradigm that is used in KeY to implement the deductive calculus.

Taclets: A New Paradigm for Constructing Interactive Theorem Provers
Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Andreas Roth, Philipp Rümmer, and Steffen Schlager
Revista de la Real Academia de Ciencias (RACSAM). Serie A: Matemáticas, 98 (1), 2004.
PDF - Abstract - BibTeX

 

A paper on the formal specification of security critical interactive applications

Formal Specification of Security-relevant Properties of User Interfaces
Bernhard Beckert and Gerd Beuster
3rd International Workshop on Critical Systems Development with UML, Lisbon, Portugal.
PDF - Abstract - BibTeX

 

This paper explores the relationship between informal Use Case descriptions and formal pre- and post-conditions. It might be the basis for an early stage in the KeY development process

From Informal to Formal Specifications in UML
Martin Giese and Rogardt Heldal
Proceedings, UML2004.
PDF - BibTeX - Abstract

 

In contrast to previous works on non-interference, our method takes into full account the weak guarantees of the Java Memory Model concerning visibility and ordering of memory updates between threads.

A JMM-Faithful Non-Interference Calculus for Java
Vladimir Klebanov
FIDJI 2004 Workshop on Scientific Engineering of Distributed Java Applications, Luxembourg
PDF (preliminary) - BibTeX - Abstract - Springer LNCS 3409

 

We describe how to simplify OCL constraints that have been automatically generated, in particular by our pattern mechanism.

Rule-Based Simplification of OCL Constraints
Martin Giese, Reiner Hähnle, and Daniel Larsson
UML2004 workshop on OCL and Model Driven Engineering, Lisbon
PDF - BibTeX - Abstract

 

Experience shows that verification attempts often fail, and that the program (and/or the specification) has to be revised. After a small change, it is better to adapt and reuse the existing partial proof than to verify the program again from first principles.

Proof Reuse for Deductive Program Verification
Bernhard Beckert and Vladimir Klebanov
Proceedings, Software Engineering and Formal Methods.
PDF (Preliminary Version) - BibTeX - Abstract

 

This paper describes a basic module concept within the KeY approach.

Ensuring Invariant Contracts for Modules in Java
Andreas Roth and Peter H. Schmitt
Proceedings, 6th Workshop on Formal Techniques for Java-like Programs - FTfJP'2004 at ECOOP 2004, University of Nijmegen, Technical Report, nr. NIII-R0426, 2004
Abstract - PDF - BibTeX

 

This paper describes the KeY-approach for data type refinement considering as example the integer data types of UML/OCL and Java.

Software Verification with Integrated Data Type Refinement for Integer Arithmetic
Bernhard Beckert and Steffen Schlager
Proceedings, Fourth International Conference on Integrated Formal Methods, Canterbury, England, 2004.
Abstract - PostScript - PDF - BibTeX - Springer-Verlag, LNCS 2999

 

2003

This paper describes how to create customised induction rules in KeY based on the idea of partition testing.

Using a Software Testing Technique to Improve Theorem Proving
Reiner Hähnle and Angela Wallenburg
Proceedings, 3rd International Workshop on Formal Approaches to Testing of Software (FATES'03), Montreal, Canada, October 2003.
Abstract - PDF - PostScript - BibTeX - FATES 2003 at Springer

 

This paper analyses the problem of constructing a deterministic proof procedure for free variable clausal tableaux that performs depth-first proof search without backtracking.

Depth-first Proof Search without Backtracking for Free-variable Clausal Tableaux
Bernhard Beckert
Journal of Symbolic Computation, Volume 36, 2003, pp 117-138.
Abstract - PostScript - BibTeX

 

Several variants of a first-order simplification rule for non-normal form tableaux using syntactic constraints are presented. These can be used as a framework for porting methods like unit resolution or hyper tableaux to non-normal form free variable tableaux. This paper differs from the FTP 2000 paper in that it contains more detailed proofs.

Simplification Rules for Constrained Formula Tableaux
Martin Giese
Proceedings, International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Rome, Italy, September 2003.
Abstract - PDF

 

This paper is an overview of a number of possible combinations between constraints and analytic tableaux presented in the literature, along with a proposal for a more differentiated and systematic nomenclature.

Tableaux + Constraints
Martin Giese and Reiner Hähnle
Position Paper, International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Rome, Italy, September 2003.
Abstract - PDF

 

This paper presents the graphical user interface of the KeY prover. In particular, it explains the role of taclets in the KeY prover from a user interface perspective. This workshop version is superseded by the extended version published in ENTCS.

Taclets and the KeY Prover
Martin Giese
Proceedings, Workshop on User Interfaces for Theorem Provers, Rome, Italy, September 2003.
Abstract - PDF

 

This paper describes an extension of the design-by-contract approach. In addition to preconditions, postconditions, and invariants as the basis for proving properties of a program, also information is provided on which parts of the state are not changed by running the program.

Program Verification Using Change Information
Bernhard Beckert and Peter H. Schmitt
Proceedings, Software Engineering and Formal Methods (SEFM), Brisbane, Australia, 2003, to appear.
Abstract - PostScript - BibTeX

 

OCL 2003 Workshop paper based on Daniel's Master's Thesis.

Specifying Java Card API in OCL
Daniel Larsson and Wojciech Mostowski
OCL 2.0 Workshop at UML, San Francisco, October 2003. Published in ENTCS (vol. 102C) in 2004.
Abstract - PDF - BibTeX - At Elsevier

 

The master thesis of Daniel Larsson discusses the development of OCL specifications for Java Card API.

OCL Specifications for the Java Card API
Daniel Larsson
Master's Thesis, Chalmers University of Technology, Department of Computing Science, Gothenburg, Sweden, 2003.
Abstract - PDF - BibTeX - Java Card API Specification

 

This paper describes a case study of an object-oriented safety critical software.

Integration of Informal and Formal Development of Object-Oriented Safety-Critical Software: A Case Study with the KeY System
Reiner Hähnle and Richard Bubel
Proceedings Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 03).
Abstract - PostScript - PDF - BibTeX

 

In this paper, the justification for a popular definition of transitive closure in terms of OCL is given.

The Definition of Transitive Closure with OCL - Limitations and Applications
Thomas Baar
PSI 2003, Andrei Ershov Fifth International Conference, Perspectives of System Informatics, Novosibirsk, Russia, 2003.
Abstract - PostScript - BibTeX

 

This paper applies the KeY interactive theorem prover to analysis of secure information flow.

A Theorem Proving Approach to Analysis of Secure Information Flow
Adam Darvas and Reiner Hähnle and Dave Sands
Workshop on Issues in the Theory of Security, WITS, 2003.
Abstract - PostScript - PDF - BibTeX

 

This is a preliminary version of the paper to appear in "Software and Systems Modeling", 2004 (see above).

The KeY Tool
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager, and Peter H. Schmitt
Department of Computing Science, Chalmers University and Göteborg University, Technical Report in Computing Science No. 2003-5, February 2003.
Abstract - PDF - BibTeX

 

This paper describes a new meta-modelling architecture aiming in the definition of UML/OCL's syntax and semantics. In opposite to the current 4-layer meta-model architecture meta-circularities are avoided.

Metamodels without Metacircularities
Thomas Baar
L'Objet, Vol. 9, No. 4, 2003, pp 95-114.
Abstract - PostScript - BibTeX

 

This paper describes how to extend KeY's verification calculus to verify "rip out" properties of Java Card programs (properties that are to be maintained in case of unexpected termination of the program) and how to handle Java Card's transaction mechanism.

A Program Logic for Handling Java Card's Transaction Mechanism
Bernhard Beckert and Wojciech Mostowski
Proceedings, Fundamental Approaches to Software Engineering.
Abstract - PostScript - BibTeX - Springer-Verlag, LNCS