Peter H. Schmitt

LOPSTR Conference 2013 Conference Paper

Information Flow in Object-Oriented Software

• Bernhard Beckert
• Daniel Bruns
• Vladimir Klebanov
• Christoph Scheben
• Peter H. Schmitt
• Mattias Ulbrich

Abstract This paper contributes to the investigation of object-sensitive information flow properties for sequential Java, i. e. , properties that take into account information leakage through objects, as opposed to primitive values. We present two improvements to a popular object-sensitive non-interference property. Both reduce the burden on analysis and monitoring tools. We present a formalization of this property in a program logic – JavaDL in our case – which allows using an existing tool without requiring program modification. The third contribution is a novel fine-grained specification methodology. In our approach, arbitrary JavaDL terms (read ‘side-effect-free Java expressions’) may be assigned a security level – in contrast to security labels being attached to fields and variables only.

JELIA Conference 2000 Invited Paper

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

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 feature of our approach is the use of a commercial CASE tool enhanced with functionality for formal specification and deductive verification.

CSL Conference 1991 Conference Paper

A Formal Operational Semantics for Languages of Type Prolog III

• Egon Börger
• Peter H. Schmitt

Abstract We use dynamic algebras introduced by Gurevich in [Gurevich 1988], [Gurevich 1991] to develop a formal semantics for the logical core of constraint logic programming languages of type Prolog III [Colmerauer 1990]. Our specification abstracts away from any particular feature of the mechanism for the resolution of constraints, thus providing a uniform description of constraint logic programming languages which turns out to be a natural refinement of the standard Prolog algebras developed in [Börger 1990]. In particular we show how our method can be used for a precise but simple method to handle specification problems connected to the freeze predicate.

ICAPS Conference 1990 Conference Paper

Modal logics for AI planning

• Jürgen Dix
• Joachim Posegga
• Peter H. Schmitt

CSL Conference 1989 Conference Paper

The Knowledge Representation Language L LILOG

• Christoph Beierle
• Jochen Dörre
• Udo Pletat
• Claus-Rainer Rollinger
• Peter H. Schmitt
• Rudi Studer

Abstract L LILOG is the knowledge representation language that is used in the LILOG project, a research project in the area of natural language understanding. L LILOG is based on full first order predicate logic and incorporates a powerful sort mechanism. Besides having a set of sorts together with an order relation on them sorts may also be defined by attribute-value pairs. Further concepts which have been included in L LILOG are reference objects for representing real world objects as well as knowledge packets for structuring knowledge bases. This paper describes the evolution of L LILOG and its basic design decisions, gives a complete abstract syntax, and provides a model theoretic semantics for the logical kernel of the language. A definition of the concrete syntax which is used in the first LILOG prototype is given in Appendix 1.

CSL Conference 1988 Conference Paper

A Survey of Rewrite Systems

• Peter H. Schmitt

CSL Conference 1988 Conference Paper

On the Computational Complexity of Quantified Horn Clauses

• Marek Karpinski
• Hans Kleine Büning
• Peter H. Schmitt

Abstract A polynomial time algorithm is presented for the evaluation problem for quantified propositional Horn clauses. This answers an open problem posed by Itai and Makowski in (IM 87).