Post-doctoral Researchers
 |
Cesar Kunz,
PhD - École des Mines de Paris (ENSMP), France
Bio | Home Page | Contact
Research Interests: Interaction between compilation and verification condition
Generators, proof carrying code.
|
 |
Mark Marron,
PhD - University of New Mexico, USA
Bio | Home Page | Contact
Research Interests: Program analysis, optimization and error detection. Development
of static analysis techniques that are capable of providing
accurate information about the behaviour of a program, in
particular the program heap.
|
 |
Daniel Hedin,
PhD - Chalmers, Sweden
Bio | Home Page | Contact
Research Interests: Programming languages: semantics, static analysis of programs in
particular type systems. Formal Proofs: practical use, modelling,
type theory, proof assistants. Security: information flow security,
declassification, language-based techniques for enforcement.
|
PhD Students
 |
Alvaro Garcia,
MS - Technical University of Madrid (UPM), Spain
Home Page | Contact
Research Interests: Type theory, dependent tpyes and genericity, in particular how to extend
dependent types in a modular way, with regardas to the expression problem.
Adviser: Pablo Nogueira (UPM)
|
 |
Miguel Angel García de Dios,
MS - Universidad Complutense, Spain
Home Page | Contact
Research Interests: Formal specification and verification, and rigorous tool supported
modeling and validation of software systems.
Adviser: Manuel Clavel
|
 |
Julian Samborski,
BS - Universidad Nacional de Rosario (UNR), Argentina
Home Page | Contact
Research Interests: Applications of Formal Methods and Abstract Interpretation to Program
Verification; Quantum Computing; Functional Programming Languages;
Semantics.
Adviser: Cesar Sanchez, Manuel Hermenegildo
|
 |
Juan Manuel Crespo,
BS - Universidad Nacional de Rosario (UNR), Argentina
Home Page | Contact
Research Interests: Programming Language Semantics, Type Theory, Functional programming,
Category Theory, Logic and Software Verification.
Adviser: Gilles Barthe
|
 |
Federico Olmedo,
BS - Universidad Nacional de Rosario (UNR), Argentina
Home Page | Contact
Research Interests: Verification of Cryptographic Systems and Semantics of Programming Languages
Adviser: Gilles Barthe
|
 |
Teresa Trigo,
MS - Technical University of Madrid (UPM), Spain
Home Page | Contact
Research Interests: Software verification techniques based on static analysis and its
application to embedded systems.Resource usage analysis and Automatic parallelization.
Adviser: Pedro Lopez-Garcia
|
 |
Antonio Artés,
MS - Technical University of Madrid (UPM), Spain
Home Page | Contact
Research Interests: Power-aware, temperature-aware and reliability-aware desing of low power semiconductor devices.
Adviser: David Atienza (UCM), J.L. Ayala (UCM) and Cesar Sanchez (IMDEA)
|
 |
Santiago Zanella,
MS - Universidad Nacional de Rosario (UNR), Argentina
Home Page | Contact
Research Interests: Formal Methods in general, and in particular in: Verification of Cryptographic Systems, Language-based Security, Semantics of Programming Languages, Type Theory, Theorem Provers and Process Calculi.
Adviser: Gilles Barthe
|
 |
Alejandro Sanchez,
BS - Universidad Nacional de Cordoba (UNC), Argentina
Home Page | Contact
Research Interests: Formal methods, program verification, dynamic memory analysis, concurrent systems, type theory, functional programming
Adviser: César Sánchez
|
Interns
 |
Carolina Dania,
BS - Universidad Nacional de Cordoba (UNC), Argentina
Home Page | Contact
Research Interests: Formal specification and verification, rigorous tool supported modeling and validation of software systems, programming languages, automation, and SAT solvers.
Adviser: Manuel Clavel
|
 |
Gerardo Huck,
BS - Universidad Nacional de Rosario (UNR), Argentina
Home Page | Contact
Research Interests: Formal methods, Functional Programming,Algorithms, Systems Design and Verification, Generic Programming,Static Analysis.
Adviser: Pedro Lopez-Garcia
|
 |
Gonzalo Ortiz,
MS - Universidad Complutense, Spain
Home Page | Contact
Research Interests: Formal specification and verification, and rigorous tool supported
modeling and validation of software systems.
Adviser: Manuel Clavel
|
|
