Dipl.-Inform. André Platzer

 

1 Theses (BibTeX Source)

@MASTERSTHESIS{Platzer_2004b,
  AUTHOR = {Platzer, Andr\'e},
  TITLE = {An Object-Oriented Dynamic Logic with Updates},
  SCHOOL = {University of Karlsruhe, Department of Computer Science. Institute for Logic, Complexity and Deduction Systems},
  YEAR = 2004,
  MONTH = {September},
  URL = {http://i12www.ira.uka.de/~key/doc/2004/odlMasterThesis.pdf},
  ABSTRACT = {
    With the goal of this thesis being to create a dynamic logic for
    object-oriented languages, ODL is developed along with a sound
    and relatively complete calculus. The dynamic logic contains only
    the absolute logical essentials of object-orientation, yet still
    allows a ``natural'' representation of all other features of
    common object-oriented programming languages. ODL is an extension
    of a dynamic logic for imperative While programs by
    function modification and dynamic type checks. A generalisation of
    substitutions, called updates, constitute the central technical
    device for dealing with object aliasing arising from function
    modification and for retaining a manageable calculus in practical
    application scenarios. Further, object enumerators realise object
    creation in a natural yet powerful way. Finally, completeness is
    proven relative to first-order arithmetic. Along with the
    soundness result, this proof constitutes the central part of this
    thesis and even copes with states containing uncomputable
    functions.}
}


@MISC{Platzer_2004,
  AUTHOR = {Platzer, Andr\'e},
  TITLE = {Using a Program Verification Calculus for
                  Constructing Specifications from Implementations},
  HOWPUBLISHED = {Minor Thesis, University of Karlsruhe, Department of
                  Computer Science. Institute for Logic, Complexity
                  and Deduction Systems},
  MONTH = {February},
  YEAR = {2004},
  SCHOOL = {University of Karlsruhe, Department of Computer
                  Science. Institute for Logic, Complexity and
                  Deduction Systems},
  URL = {http://www.functologic.com/logic/Minoranthe.pdf},
  ABSTRACT = { In this paper we examine the possibility of
                  automatically constructing the program specification
                  from an implementation, both from a theoretical
                  perspective and as a practical approach with a
                  sequent calculus. As a setting for program
                  specifications we choose dynamic logic for the Java
                  programming language. We show that---despite the
                  undecidable nature of program analysis---the
                  strongest specification of any program can always be
                  constructed algorithmically. Further we outline a
                  practical approach embedded into a sequent calculus
                  for dynamic logic and with a higher focus on
                  readability. Therefor, the central aspect of
                  describing unbounded state changes incorporates the
                  concept of modifies lists for expressing the
                  modifiable portion of the state space. The
                  underlying deductions are carried out by the theorem
                  prover of the KeY System.}
}