Specification Predicates with Explicit Dependency Information (2009)
Richard Bubel, Reiner Hähnle, Peter H. Schmitt
Abstract. Specifications of programs use auxiliary symbols to encapsulate concepts for a variety of reasons: readability, reusability, structuring and, in particular, for writing recursive...
Verification of Modifies Clauses in Dynamic Logic with Non-rigid Functions (2009)
Engel, Christian, Roth, Andreas, Schmitt, Peter H., Weiß, Benjamin
Benjamin Weiß, Betreuer Prof, H. Schmitt, Fakultät Für Informatik, Ich Betreuer, ...
besonderer Dank gilt außerdem Richard Bubel für die vielen hilfreichen Anregungen, die ich von ihm bekam; Achim Kuwertz für seine Arbeit an der SMT-Schnittstelle; Margarete Sackmann fürs...
A Sequent Calculus for a First-order Dynamic Logic with Trace Modalities for Promela + (2008)
Florian Rabe, Steffen Schlager, Peter H. Schmitt
Abstract. In this paper we introduce the first-order dynamic logic DLP for Promela +, a language subsuming the modelling language Promela of the Spin model checker. In DLP trace modalities can be...
Peter H. Schmitt, Frank Werner, Fakultät Für Informatik
Abstract. Networking and power management of wireless energy- conscious sensor networks is an important area of current research. We investigate a network of MicaZ sensor motes using the ZigBee...
EADS Innovations Works, (2008)
Prof Dr, Peter H. Schmitt, Natascha Scharnberg, Prof Dr, Peter H. Schmitt, ...
durchgeführt bei
A Sequent Calculus for a First-order Dynamic Logic with Trace Modalities for Promela + (2008)
Florian Rabe, Steffen Schlager, Peter H. Schmitt
Abstract. We introduce the first-order dynamic logic DLP for Promela +, a language subsuming the modelling language Promela of the Spin model checker. In DLP trace modalities can be used to reason...
Verifying Object-Oriented Programs with KeY: A Tutorial (2008)
Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt
Abstract. This paper is a tutorial on performing formal specification and semi-automatic verification of Java programs with the formal software development tool KeY. This tutorial aims to fill the...
Verifying Object-Oriented Programs with KeY: A Tutorial (2008)
Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt
Abstract. This paper is a tutorial on performing formal specification and semi-automatic verification of Java programs with the formal software development tool KeY. This tutorial aims to fill the...
The ASMKeY Theorem Prover (2008)
Stanislas Nanchen, Hubert Schmid, Peter H. Schmitt, Robert Stärk
Abstract. In [8], we presented a logic for Abstract State Machines (ASMs). In this technical report, we present an interactive theorem prover call ASMKeY where we implemented this logic. We also...
Inferring Invariants by Symbolic Execution (2008)
Peter H. Schmitt, Benjamin Weiß
Abstract. In this paper we propose a method for inferring invariants for loops in Java programs. An example of a simple while loop is used throughout the paper to explain our approach. The method is...
KeY: A Formal Method for Object-Oriented Systems (2008)
Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt
Abstract. This paper gives an overview of the KeY approach and highlights the main features of the KeY system. KeY is an approach (and a system) for the deductive verification of object-oriented...
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, ...
Abstract KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal...
Tool support for OCL and related formalisms - needs and trends (2008)
Thomas Baar, Dan Chiorean, Re Correa, Martin Gogolla, Heinrich Hußmann, Octavian Patrascoiu, ...
Abstract. The recent trend in software engineering to model-centered methodologies is an excellent opportunity for OCL to become a widely used specification language. If the focus of the development...
The Even More Liberalized δ-Rule in Free Variable Semantic Tableaux (2008)
Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt
. In this paper we have a closer look at one of the rules of the tableau calculus presented in [3], called the ffi--rule, and the modification of this rule, that has been proved to be sound and...
A Description of the Tableau Method Using Abstract State Machines (2007)
Peter H. Schmitt, Egon Börger, Egon B
State Maschines 1 Peter H. SCHMITT, Institute for logic, complexity and deductive systems, Department of Computer Science, University of Karlsruhe, D 76128 Karlsruhe, Germany E-mail:...
The Approach: Integrating Object Oriented Design and Formal Veri cation (2007)
Wolfgang Ahrendt Thomas, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Wolfram Menzel, ...
. This paper reports on the ongoing KeY project aimed at bridging the gap between (a) OO software engineering methods and tools and (b) deductive verication. A distinctive feature of our approach is...
FASE System Description The System: Integrating Object-Oriented Design and Formal Methods ⋆ (2007)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Reiner Hähnle, Wolfram Menzel, ...
Abstract. 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...
of Karlsruhe. The goal of this project is to introduce the support of teaching and learning through multimedia technology. We will in particular address the issue of information systems,...
Thomas Baar, Bernhard Beckert, Peter H. Schmitt
Abstract. We consider rst-order Dynamic Logic (DL) with non-rigid functions, which can be used to model certain features of programming languages such as array variables and object attributes. We...
Ensuring Invariant Contracts for Modules in Java (2007)
Andreas Roth, Peter H. Schmitt
Abstract. Deductive verification of object-oriented programs suffers from the lack of modularity. One of the obstacles to modular verification are invariant contracts, which classes extending a...
Technical Report no. 2003-05 The KeY Tool 1 (2007)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, ...
KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal methods and...
Implementing semantic tableaux. (2007)
Posegga, Joachim, Schmitt, Peter H.
This report describes implementions of the tableau calculus for first-order logic. First an extremely simple implementation, called leanTAP, is presented, which nonetheless covers the full...
Proving WAM compiler correctness. (2007)
In this note we analyse the proof of compiler correctness of the WAM given in the paper The WAM - Definition and Compiler Correctness by Egon Boerger and Dean Rosenzweig. TR-14/92, Dipartimento di...
The KeY System 1.0 (deduction component (2007)
Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Steffen Schlager, Peter H. Schmitt
www.key-project.org Abstract. The KeY system is a development of the ongoing KeY project, whose aim is to integrate formal specification and deductive verification into the industrial software...
The KeY System 1.0 (deduction component (2007)
Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Steffen Schlager, Peter H. Schmitt
www.key-project.org Abstract. The KeY system is a development of the ongoing KeY project, whose aim is to integrate formal specification and deductive verification into the industrial software...
The KeY System 1.0 (deduction component (2007)
Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Steffen Schlager, Peter H. Schmitt
www.key-project.org Abstract. The KeY system is a development of the ongoing KeY project, whose aim is to integrate formal specification and deductive verification into the industrial software...
Verifying the Mondex case study (2007)
www.key-project.org 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...
Model Checking for Energy Efficient Scheduling in Wireless Sensor Networks (2006)
Schmitt, Peter H., Werner, Frank
Networking and power management of wireless energy - conscious sensor networks is an important area of current research. We investigate a network of MicaZ sensor motes using the ZigBee protocol for...
Christian Engel, Responsible Supervisor, Prof Dr, Peter H. Schmitt, Supervisor Prof, Dr. Reiner Hähnle, ...
At this place I would like to thank everyone who supported me in creation of this thesis. First of all, I am very grateful to Prof. Dr. Peter H. Schmitt and Prof. Dr. Reiner Hähnle for their...
An improved rule for while loops in deductive program verification (2005)
Beckert, Bernhard, Schlager, Steffen, Schmitt, Peter H.
The performance and usability of deductive program verification systems can be greatly enhanced if specifications of programs and program parts not only consist of the usual pre-/post-condition pairs...
Ahrendt, Wolfgang, Baar, Thomas, Beckert, Bernhard, Bubel, Richard, Giese, Martin, Hähnle, Reiner, ...
KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal methods and...
OCL and Model Driven Engineering (2005)
Bézivin, Jean, Baar, Thomas, Gardner, Tracy, Gogolla, Martin, Hähnle, Reiner, Hussmann, Heinrich, ...
Precise modeling is essential to the success of the OMG's Model Driven Architecture initiative. At the modeling level (M1) OCL allows for the precision needed to write executable models. Can OCL be...
An improved rule for while loops in deductive program verification (2005)
Bernhard Beckert, Steffen Schlager, Peter H. Schmitt
Abstract. The performance and usability of deductive program verification systems can be greatly enhanced if specifications of programs and program parts not only consist of the usual...
An object-oriented dynamic logic with updates (2004)
André Platzer, Responsible Supervisor, Prof Dr, Peter H. Schmitt, Supervisor Dr. Bernhard Beckert
With the goal of this thesis being to create a dynamic logic for objectoriented languages, ODL is developed along with a sound and relatively complete calculus. The dynamic logic contains only the...
Hans-joachim Daniels, Fakultät Für Informatik, Verantwortlicher Betreuer, Prof Dr, Peter H. Schmitt, ...
Thanks to Peter H. Schmitt and Reiner Hähnle, they made it possible that I could write
Program verification using change information (2003)
Bernhard Beckert, Peter H. Schmitt
i12www.ira.uka.de/key 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, also...
Program verification using change information (2003)
Bernhard Beckert, Peter H. Schmitt
i12www.ira.uka.de/˜key 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, also...
The KeY system: Integrating object-oriented design and formal methods (2002)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Elmar Habermalz, Wolfram Menzel, Wojciech Mostowski, ...
Abstract. 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...
Translating the Object Constraint Language into First-order Predicate Logic (2002)
Bernhard Beckert, Uwe Keller, Peter H. Schmitt
Abstract. In this paper, we define a translation of UML class diagrams with OCL constraints into first-order predicate logic. The goal is logical reasoning about UML models, realized by an...
Translating the Object Constraint Language into First-order Predicate Logic (2002)
Bernhard Beckert, Uwe Keller, Peter H. Schmitt
Abstract. In this paper, we define a translation of UML class diagrams with OCL constraints into first-order predicate logic. The goal is logical reasoning about UML models. We put an emphasis on...
Translating the Object Constraint Language into First-order Predicate Logic (2002)
Bernhard Beckert, Uwe Keller, Peter H. Schmitt
Abstract. In this paper, we define a translation of UML class diagrams with OCL constraints into first-order predicate logic. The goal is logical reasoning about UML models, realized by an...
A model theoretic semantics of OCL (2001)
i12www.ira.uka.de/~pschmitt Abstract. This paper proposes a model theoretic semantics of the Object Constraint Language (OCL), strictily observing the OCL standard. 1
Abstract We introduce a new logic for nite rst-order structures with a linear odering. We study its expressive power. In particular we show that it is strictly stronger than rst-order logic on nite...
An Extension of Dynamic Logic (2001)
For Modelling Ocl's, Thomas Baar, Bernhard Beckert, Peter H. Schmitt
We consider rst-order Dynamic Logic (DL) with non-rigid functions, which can be used to model certain features of programming languages such as array variables and object attributes. We extend this...
The KeY approach: integrating object oriented design and formal verification. (2000)
Ahrendt, Wolfgang, Baar, Thomas, Beckert, Bernhard, Giese, Martin, Habermalz, Elmar, Haehnle, Reiner, ...
This paper reports on the ongoing KeY project aimed at bridging the gap between (a) OO software engineering methods and tools and (b) deductive verification. A distinctive feature of our approach is...
The KeY approach: integrating object oriented design and formal verification. (2000)
Ahrendt, Wolfgang, Baar, Thomas, Beckert, Bernhard, Giese, Martin, Habermalz, Elmar, Haehnle, Reiner, ...
The KEY Approach: Integrating Object Oriented Design and Formal Verification (2000)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, ...
This paper reports on the ongoing KeY project aimed at bridging the gap between (a) OO software engineering methods and tools and (b) deductive verification. A distinctive feature of our approach is...
The KeY Approach: Integrating Object Oriented Design and Formal Verification (2000)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Wolfram Menzel, ...
Abstract This paper reports on the ongoing KeY project aimed at bridging the gap between (a) object-oriented software engineering methods and tools and (b) deductive verification. A distinctive...
Nikolaj S. Bjørner, Reiner Hähnle, Wolfram Menzel, Wolfgang Reif, Peter H. Schmitt, Wolfram Menzel (karlsruhe, ...
This paper highlights a project to integrate interactive and automated theorem proving in Software Verification. Its aim is to combine the advantages of the two paradigms. We focus on one particular...
A tableau system for linear temporal logic (1997)
Peter H. Schmitt, Jean Goubault-larrecq
We present a sound, complete and terminating tableau system for the propositional logic of linear time with only 2 and 3 as temporal operators. 1
A Tableau System for Linear Temporal Logic (1997)
Peter H. Schmitt, Jean Goubault-larrecq
We present a sound, complete and terminating tableau system for the propositional logic of linear time with only 2 and 3 as temporal operators. 1 Introduction Deduction calculi for propositional...
A Tableau System for Full Linear Temporal Logic (1997)
Peter H. Schmitt, Jean Goubault-larrecq
We present a sound, complete and terminating tableau system for the propositional logic of linear time with 2, 3, fl, W and U and the past operators 2 - , 3 - , fl\Gamma , e fl\Gamma , B and S. ffl...
A Description of the Tableau Method Using Abstract State Machines (1997)
BÖRGER, EGON, SCHMITT, PETER H.
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...
A Tableau Calculus for First-Order Branching Time Logic (1996)
Wolfgang May, Peter H. Schmitt
. Tableau-based proof systems have been designed for many logics extending classical first-order logic. This paper proposes a sound tableau calculus for temporal logics of the first-order CTL-family....
Universitat Karlsruhe Fakultat fur Informatik (1996)
Implementing Semantic Tableaux, Interner Bericht, Fakultat Fur Informatik, Joachim Posegga, Joachim Posegga, Peter H. Schmitt, ...
This report will appear as a chapter in the
Implementing Semantic Tableaux (1996)
Interner Bericht, Fakultat Fur Informatik, Joachim Posegga, Joachim Posegga, Peter H. Schmitt, Peter H. Schmitt
This report will appear as a chapter in the
A Tableau Calculus For First-Order Branching Time Logic (1996)
Wolfgang May, Peter H. Schmitt
Abstract. Tableau-based proof systems have been designed for many logics extending classical rst-order logic. This paper proposes a sound tableau calculus for temporal logics of the rst-order...
Automated Deduction with Shannon Graphs (1995)
Joachim Posegga, Peter H. Schmitt
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....
Automated Deduction with Shannon Graphs (1995)
POSEGGA, JOACHIM, SCHMITT, PETER H.
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 even more liberalized δ-rule in free variable semantic tableaux (1993)
Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt
Abstract. In this paper we have a closer look at one of the rules of the tableau calculus presented in [3], called the δ–rule, and the modification of this rule, that has been proved to be sound...
Model theory of ordered abelian groups. (1982)
Heidelberg, Univ., Habil.-Schr., 1983 (Nicht f.d. Austausch).