Leonor Prensa Nieto

INRIA-Sophia Antipolis
Projet LEMME
2004 Route des Lucioles, BP 93
06902 Sophia Antipolis Cedex
France
Tél: (33) 4 92 38 77 98
Fax: (33) 4 92 38 50 60
Email: Leonor.Prensa@sophia.inria.fr

Education

Master (licenciatura) in Mathematics with speciality in Computer Science at the Facultad de Ciencias Matemáticas, Universidad Complutense de Madrid, June 1997.

Doctoral Thesis in Computer Science at the Fakultät für Informatik, Technische Universität München, February 2002.
My supervisors were Tobias Nipkow and Javier Esparza. I was a member of the Theorem Proving Group and of the PhD programm Logic in Computer Science.

Since September 2002 I am a post-doc at INRIA-Sophia Antipolis in the LEMME group. I am working in the Profundis and Verificard projects.

Research interests

Specification and verification of parallel programs.

Automatic and interactive theorem proving.

Semantics.

Type systems for security.

Publications

Leonor Prensa Nieto. The Rely-Guarantee Method in Isabelle/HOL. European Symposium on Programming (ESOP'03), LNCS 2618, pages 348-362. Springer-Verlag, 2003.

Leonor Prensa Nieto. Verification of Parallel Programs with the Owicki-Gries and Rely-Guarantee Methods in Isabelle/HOL. PhD Thesis. Technische Universität München, 2002.

Leonor Prensa Nieto. Completeness of the Owicki-Gries System for Parameterized Parallel Programs. Formal Methods for Parallel Programming: Theory and Applications (FMPPTA'01). IEEE CS Press, 2001.

Leonor Prensa Nieto, Javier Esparza. Verifying Single and Multi-mutator Garbage Collectors with Owicki-Gries in Isabelle/HOL. 25th International Symposium on Mathematical Foundations of Computer Science (MFCS'00), LNCS 1893, pages 619-628. Springer-Verlag, 2000.

Leonor Prensa Nieto, Javier Esparza. Verifying garbage collection algorithms with Owicki/Gries in Isabelle/HOL. Requirements, Design, Correct Construction and Verification., volume 11 of Softwaretechnik Reihe der Forschungsinstitut für Angewandte Softwaretechnologie (FAST), pages 49-58. Verlag Uni-Druck, 2000.

Tobias Nipkow, Leonor Prensa Nieto. Owicki/Gries in Isabelle/HOL. Fundamental Approaches to Software Engineering (FASE'99), LNCS 1577, pages 188-203. Springer-Verlag, 1999.

Software

Leonor Prensa Nieto. The Isabelle session Isabelle/HOL/HoareParallel contains a set of theories, proof scripts and ML code which forms a tool for the verification of parallel programs with the Owicki-Gries and Rely-Guarantee methods. Many examples are included. See the joint document.

Tobias Nipkow, Leonor Prensa Nieto and Norbert Galm. The Isabelle session Isabelle/HOL/Hoare contains a set of theories, proof scripts and ML code which forms a tool for the verification of sequential programs wiht the classic Hoare logic. See the joint explanation.