Enforcing High-Level Security Properties for Applets. - Mariela Pavlova; Gilles Barthe; Lilian Burdy; Marieke Huisman; Jean-Louis Lanet (CARDIS, 2004)

Precise Analysis of Memory Consumption using Program Logics. - Gilles Barthe; Mariela Pavlova; Gerardo Schneider (SEFM, 2005)

A Low-Footprint Java-to-Native Compilation Scheme Using Formal Methods. - Alexandre Courbot; Mariela Pavlova; Gilles Grimaud; Jean-Jacques Vandewalle (CARDIS, 2006)

JACK - A Tool for Validation of Security and Behaviour of Java Applications. - Gilles Barthe; Lilian Burdy; Julien Charles; Benjamin Grégoire; Marieke Huisman; Jean-Louis Lanet; Mariela Pavlova; Antoine Requet (FMCO, 2006)

Java bytecode specification and verification. - Lilian Burdy; Mariela Pavlova (SAC, 2006)

Preliminary Design of BML: A Behavioral Interface Specification Language for Java Bytecode. - Lilian Burdy; Marieke Huisman; Mariela Pavlova (FASE, 2007)

Certification Using the Mobius Base Logic. - Lennart Beringer; Martin Hofmann 001; Mariela Pavlova (FMCO, 2007)

Elimination of Ghost Variables in Program Logics. - Martin Hofmann 001; Mariela Pavlova (TGC, 2007)

Preservation of Proof Obligations from Java to the Java Virtual Machine. - Gilles Barthe; Benjamin Grégoire; Mariela Pavlova (IJCAR, 2008)