Mariela Pavlova

Organization:	INRIA
Research Unit:	Sophia Antipolis
Project:	Everest
Phone:	(+33/04) 92 38 75 65
Fax:	(+33/04) 92 38 50 60
E-mail:	Mariela dot Pavlova at sophia dot inria dot fr	( replace dot by . and at by @ )

Research Interests

Program Logic and Verification
Specification language
Program Language Semantics
Weakest precondition calculus.
Proof carrying code.

Current 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

Enforcing High Level Security Properties For Applets, M. Pavlova, G. Barthe, L. Burdy, M. Huisman, and J.-L. Lanet, IFIP 18th World Computer Congress 2004, Smart Card Research and Advanced Applications (CARDIS), Toulouse, France

Precise Analysis of Memory Consumption Using Program Logic, G. Barthe, M. Pavlova, and G. Schneider, In B. Aichernig and B. Beckert, editors, Proceedings of SEFM'05, pages 86-95, IEEE Computer Society press

Java Bytecode Specification and Verification, Lilian Burdy and Mariela Pavlova, In L.M. Liebrock, editor, proceedings of SAC 2006. ACM

A low-footprint Java-to-Native Compilation Scheme using Formal Methods, A. Courbot, M. Pavlova, G. Grimaud, and J.J. Vandewalle, proceedings of CARDIS, volume 3928 of Lecture Notes in Computer Science, pages 329-344. Springer, 2006

Preliminary design of BML: a behavioral interface specification language for Java bytecode, Lilian Burdy, Marieke Huisman, and Mariela Pavlova, In Fundamental Approaches to Software Engineering (FASE 2007), volume 4422 of Lecture Notes in Computer Science, pages 215-229. Springer-Verlag, 2007

Technical Drafts

Compiling JML specifications

Java Bytecode Specification and Logic

PhD thesis

Java bytecode verification and its applications

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.
Who am I working with ?
My advisors are Gilles Barthe and Lilian Burdy.
Master Thesis

Automatic generation of JML specification for Java Card applications. DEA Report, Université Paris VII - Denis Diderot, 2003.