Mariela Pavlova



Organization: LMU
Chair: Theoretical Computer Science
Phone: (+49) 89 21 80 93 09
E-mail: Mariela dot Pavlova at tcs dot ifi dot lmu dot de ( replace dot by . and at by @ )


Research Interests

Recent work

  • Elimination of ghost variables in program logics
  • Formalization in Coq of the relation between a standard and ghost partial logics
    Formalization in Coq of the relation between a standard and ghost trace logics

    Publications



    Technical Drafts

    PhD thesis

    What was My Phd Thesis About ?

    I have been working with Lilian Burdy on the definition and the implementation of a framework for Java bytecode program verification. This involves the definition of a bytecode specification language and a compiler from the high level specification language JML(the Java Modeling Language) to the bytecode specification language. In order to perform bytecode verification we define a bytecode verification condition generator. The latter is based on a weakest precondition calculus defined for almost all sequential bytecode instructions (except for 64 bytes data and floating point arithmetic). We have both the implementations of the weakest precondition calculus and the JML compiler. They are integrated into the JACK (Java Correctnes Kit ) eclipse plugin.

    Master Thesis