|
Older Publications
INDEX: 2002 2001 2000
1999
- In this paper, some similarities between test cases and formal specifications are
discussed. In particular, we propose a categorisation of specifications with respect to
executability.
- Executable and Symbolic Conformance Tests for Implementation Models
Thomas Baar
Proceedings of OOIS 2002, Workshop Model-Driven Approaches to Software Development,
Montpellier, France, September 2002.
Abstract - PDF at Springer
- BibTeX -
- Andreas Roth's diploma thesis on the Java Collections Framework covering aspects of
refinement when working with UML/OCL and the KeY system.
- Deduktiver Softwareentwurf am Beispiel des Java Collections Framework -
Verfeinerungsbeziehungen in UML/OCL
Andreas Roth
Diploma thesis, University of Karlsruhe, Department of Computer Science, 2002. In German.
PostScript -
PDF - BibTeX -
- This paper describes an approach which aims at identifying false conjectures about free
data types.
- Deductive Search for Errors in Free Data Type Specifications using Model
Generation
Wolfgang Ahrendt
Automated Deduction - CADE-18, 18th International Conference on Automated Deduction
Copenhagen, Denmark, July 2002. Springer, LNCS 2392.
Abstract
- PostScript - BibTeX -
- This paper describes the translation of the OCL into first-order logic used in the KeY
system.
- Translating the Object Constraint Language into First-order Predicate Logic
Bernhard Beckert, Uwe Keller, and Peter H. Schmitt
Proceedings of VERIFY, Workshop at Federated Logic Conferences (FLoC), Copenhagen,
Denmark, 2002.
Abstract - PostScript - BibTeX -
- This paper describes the KeY approach to handing integer arithmetic.
- Integer Arithmetic in the Specification and Verification of Java Programs
Bernhard Beckert and Steffen Schlager
Proceedings of Workshop on Tools for System Design and Verification, Günzburg, Germany,
2002.
Abstract - PostScript - BibTeX -
- In the diploma thesis of Steffen Schlager, problems of integer arithmetic in the
verification of Java programs are investigated and an approach for their solution is
presented.
- Behandlung von Integer-Arithmetik bei der Verifikation von Java-Programmen
Steffen Schlager
Diploma Thesis, University of Karlsruhe, Department of Computer Science, Mai 2002.
In German - English version -
- This paper gives a completeness proof for a style of automated equality handling that is
likely to be used in the KeY prover.
- A Model Generation Style Completeness Proof for Constraint Tableaux with
Superposition
Martin Giese
Proceedings, International Conference on Automated Reasoning with Analytic Tableaux and
Related Methods, Copenhagen, Denmark, August 2002.
Abstract - PDF - BibTeX -
- This paper proposes the language CINV as a core of UML/OCL. CINV serves as a meta
language for the precise definition of UML's syntax and semantics.
- How to Ground Meta-Circular OCL Descriptions - a Set-Theoretic Approach -
Thomas Baar
Proceedings of ROOM4 workshop, London, 2002.
Abstract - PostScript - BibTeX -
- This paper presents an approach to rigorous, tool supported design and development of
Java Card applications in connection with the KeY system.
- Rigorous development of Java Card applications
Wojciech Mostowski
Proceedings of ROOM4 workshop, London, 2002.
Abstract - PostScript - BibTeX -
- This paper describes the current state of the KeY system from a tool demo perspective.
Note that there is a more detailed description of the system on our download page.
- The KeY System: Integrating Object-Oriented Design and Formal Methods
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Reiner Hähnle, Wolfram
Menzel, Wojciech Mostowski and Peter H. Schmitt
Proceedings of FASE at ETAPS 02, Grenoble, France, 2002.
Abstract - PDF - Appendix - BibTeX -
- This paper describes the design and implementation of an authoring tool for software
requirements specifications in both, natural language and OCL. It will be integrated in
the KeY tool in the future.
- An Authoring Tool for Informal and Formal Requirements Specifications
Reiner Hähnle, Kristofer Johannisson and Aarne Ranta
Proceedings of FASE at ETAPS 02, Grenoble, France, 2002.
Abstract - PostScript - PDF - BibTeX -
- In this paper, we introduce a new logic for finite first-order structures with a linear
odering, and we study its expressive power.
- Iterate Logic
Peter H. Schmitt
Proof Theory in Computer Science, Proceedings, International Seminar, Dagstuhl Castle,
Germany, 2001.
Abstract - PostScript - BibTeX -
- In this paper, we present the theoretical foundations to extend the concept of
free-variable semantic tableaux to propositional modal logics.
- Free-variable Tableaux for Propositional Modal Logics
Bernhard Beckert and Rajeev Goré
Studia Logica, Volume 69, 2001, pp 59-96.
Abstract - BibTeX -
- In this paper, we describe how Java's abrupt termination is handled in the Dynamic Logic
for Java Card that has been developed within the KeY project.
- Handling Java's Abrupt Termination in a Sequent Calculus for Dynamic Logic
Bernhard Beckert and Bettina Sasse
Proceedings, IJCAR Workshop on Precise
Modelling and Deduction for Object-oriented Software Development, Siena, Italy, 2001.
Abstract - PostScript - BibTeX -
- This paper proposes a model theoretic semantics of the Object Constraint Language (OCL),
observing the OMG standard as close as possible.
- A Model Theoretic Semantics of OCL
Peter H. Schmitt
Proceedings, IJCAR Workshop on Precise
Modelling and Deduction for Object-oriented Software Development, Siena, Italy, 2001.
PostScript - BibTeX -
- This paper presents a method for proof search without backtracking in free variable
analytic tableaux that incrementally comutes sets of closing instantiations.
- Incremental Closure of Free Variable Tableaux
Martin Giese
Proceedings, International Joint Conference on Automated Reasoning, Siena, Italy, 2001.
Abstract - PostScript - PDF - BibTeX -
- In this paper, Dynamic Logic is extended with an operator similar to OCL's @pre
operator. It is shown that formulas with this operator can be transformed into equivalent
formulas of the non-extended logic.
- An Extension of Dynamic Logic for Modelling OCL's @pre Operator
Thomas Baar, Bernhard Beckert, and Peter H. Schmitt
Proceedings, Fourth Andrei Ershov International Conference, Perspectives of System
Informatics.
Abstract - PostScript - BibTeX -
- In this paper, Dynamic Logic is extended with additional trace modalities
"throughout" and "at least once", which refer to all the states a
program reaches. A sound and (relatively) complete sequent calculus for this extended
Dynamic Logic is given.
- A Sequent Calculus for First-order Dynamic Logic with Trace Modalities
Bernhard Beckert and Steffen Schlager
Proceedings, International Joint Conference on Automated Reasoning, Siena, Italy, 2001.
Abstract - PostScript - BibTeX - Springer Verlag, LNCS -
- This paper is a description of a Dynamic Logic for Java Card and a sequent calculus for
this logic, which is the basis for the KeY system's software verification component.
- A Dynamic Logic for the Formal Verification of Java Card Programs
Bernhard Beckert
Java on Smart Cards: Programming and Security. Revised Papers, Java Card 2000,
International Workshop, Cannes, 2000.
Abstract - PostScript - BibTeX - Springer Verlag, LNCS -
- This paper addresses the problems of making program specifications written in OCL easier
to read and to maintain. The solution proposed is to use the grammar formalism GF.
- Connecting OCL with the Rest of the World
Reiner Hähnle and Aarne Ranta
Proceedings, WTUML: Workshop on Transformations in UML at ETAPS, Genova, Italy, April
2001.
Abstract - PostScript - BibTeX -
- This paper describes the project's goals and its state at the time of writing.
- The KeY Approach:
Integrating Object Oriented Design and Formal Verification
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner
Hähnle, Wolfram Menzel, Peter H. Schmitt
Proceedings, 8th European Workshop on Logics in AI (JELIA), Malaga, Spain, September 2000
(an earlier version appeared as Technical
Report 2000/4, University of Karlsruhe, Department of Computer Science, January 2000).
Abstract - PostScript - PDF - BibTeX -
- This paper uncovers some ambiguities within the definition of OCL. To overcome most of
that problems, a new metamodel of OCLs typesystem is proposed.
- An Integrated Metamodel for OCL Types
Thomas Baar and Reiner Hähnle
OOPSLA 2000 Workshop Refactoring the UML: In Search of the Core, Minneapolis,
Minnesota, USA.
Abstract -
Postscript - PDF - Bibtex -
- This paper relates Abstract State Machines (ASMs) with a particular diagram type of UML,
the State Transition Diagrams (STDs). The principles of translating ASMs into STDs are
discussed and demonstrated in four case studies.
- Embedding ASMs into State Transition Diagrams
Theo Sattler and Wolfgang Ahrendt
Technical Report 2000/20, University of Karlsruhe, Department of Computer Science, 2000.
PostScript,
PDF, plain text, and graphical version - Bibtex - This paper describes several variants of a first-order simplification rule for
non-normal form tableaux using syntactic constraints. They can be used as a framework for
porting refinements of clausal first-order proof procedures to non-normal form tableaux.
- A First-order Simplification Rule with Constraints
Martin Giese
Proceedings, International Workshop on First-Order Theorem Proving,
St. Andrews, Scotland, 2000.
Abstract - Postscript - PDF - Bibtex - The Instance Stream approach for automated theorem proving without backtracking in
free-variable tableaux is briefly presented.
- Proof Search without Backtracking using Instance Streams, Position Paper
Martin Giese
Proceedings, International Workshop on First-Order Theorem Proving, St. Andrews, Scotland,
2000.
Abstract - Postscript - PDF - Bibtex - This paper presents a calculus, intended to search for models of free data type
specifications. This constitutes a basis for disproving conjectures about consistent free
data types.
- A Basis for Model Computation in Free Data Types
Wolfgang Ahrendt
Proceedings, CADE-17 Workshop on Model Computation - Principles, Algorithms, Applications,
Pittsburgh, Pennsylvania, USA, 2000.
Abstract - Postscript - PDF - Bibtex - 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
Proceedings, International Workshop on First-Order Theorem Proving,
St. Andrews, Scotland, 2000.
Abstract - Postscript - PDF - Bibtex
An updated version of this paper is going to appear in the Journal of Symbolic Computation
(see above). - This paper is a short description of a Dynamic Logic for Java Card and a sequent
calculus for this logic, which is the basis for the KeY system's software verification
component.
- A Dynamic Logic for Java Card
Bernhard Beckert
Proceedings, 2nd ECOOP Workshop on Formal Techniques for Java Programs,
Cannes, France, 2000.
Abstract - Postscript - PDF - Bibtex - This paper describes the enrichment of design patterns with OCL constraint schemata.
Based on experiences within an industrial project it is shown how this technique can
facilitate writing formal specifications.
- Entwurfsmustergesteuerte Erzeugung von OCL-Constraints
Thomas Baar, Reiner Hähnle, Theo Sattler, Peter H. Schmitt
Informatik 2000, 30. Jahrestagung der Gesellschaft für Infomatik, Berlin, Germany. In
German.
Abstract
- Postscript - PDF - Bibtex - This paper uncovers pitfalls for software developers unexperienced with OCL.
- Experiences with the UML/OCL-Approach in Practice and Strategies of Overcome
Deficiencies
Thomas Baar
Net.ObjectDays 2000, Erfurt, Germany.
Abstract - Postscript - PDF - Bibtex - The master thesis of Theo Sattler investigates the application of design patterns and
OCL constraints in an industrial context.
- Einbindung formaler Constraints in UML Spezifikationen
Theo Sattler
Master's Thesis, University of Karlsruhe, Department of Computer Science, January 2000.
In German.
Postscript - PDF - Bibtex - The concept described in this paper will be integrated into the theorem prover used in
the KeY project (this concept was first implemented in the theorem prover IBIJa).
- Interactive Theorem Proving with Schematic Theory Specific Rules
Elmar Habermalz
Submitted, January 2000.
Abstract - PostScript - PDF - BibTeX - IBIJa home page
- A short survey of the project goals.
- Integrierter deduktiver Software-Entwurf
Reiner Hähnle, Wolfram Menzel, Peter H. Schmitt
KI, Issue 4/98 (December), pp. 40-41, 1998. In German.
Abstract - PostScript - PDF - BibTeX
|
