At the
INRIA swimming-pool

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.