Diego Garbervetsky

Diego Garbervetsky | Homepage

Dr. Diego Garbervetsky

FTA Professor @ LaFHIS, DC, FCEyN, Universidad de Buenos Aires

About

Dr. Diego Garbervetsky

I am a Full-time Professor at the Computer Science Department, School of Sciences, University of Buenos Aires.
I am also a Researcher at CONICET [CV (in spanish)].

Currently I am also in charge of the Secretary of Research and Technology Transfer in our CS Department (with Flavia Bonomo).

I am interested in automatic program analysis. I am currently working in static analysis aimed at resource usage analysis of Java-like programs, automated program verification, program understanding and validation.

News

FSE 2014

  • I am publicity co-chair for South-America of FSE 2014. Now open for submissions
  • We are hiring! Please contact me for PhD and Posdoc opportunities.
  • I gave an invited talk about quantitative analysis of heap memory consumption at SEIF Brazil workshop.

Research

Current researh interests are in Program analysis (in particular):

  • Automatic symbolic resource analysis (dynamic memory, energy, etc)
  • Program understanding.
  • Static analysis aimed at program verification of Java like programs.

Publications

My PhD Thesis: Parametric specifications of dynamic memory utilization, advisors: Victor Braberman (DC-FCEN-UBA) and Sergio Yovine (Verimag-CNRS/CONICET)

Teaching

Currently: Algoritmos y Estructuras de Datos 1

Previously: Automatic Software Validation and Verification, Automatic Program Analysis, Ingeniería de Software 2, Paradigmas de Lenguajes de Programación, Organizacion del Computador 1 (verano).

Phd Students

Former Phd Students

Undergraduate Students (simil to MSc thesis)

Some offered thesis topics: Enablabledness models, Resource Analysis, Modular Verification,Bounded Verification

Currently:
Jose Cacherosky (co-advisor A. Ketterlin)

Previous students (link to their thesis):

Tools

Automatic abstraction for behavior validation:

  • Contractor: An automated tool that takes a software contract or an API source code and generates a finite abstract representation useful for its validation
  • Contractor.NET: A Visual Studio extension for .NET validation and specification strengthening.

Analysis of heap memory consumption:

  • JConsume2: A compositional analysis for inferring heap memory consumption in Java (now available for download!).
  • Resource Contracts.NET: An extenstion of Code Contracts to specify and verify memory consumption constraints in .NET programs.
  • JConsume: An automatic memory consumption analyzer for Java (not available for download yet).
  • JScoper: An Eclipse plug-in that assist transalation of Java applications to Java Real Time ones.

Verification:

  • BudaPest: An automated software verifier of imperative programs.
  • VInTime: A tool suite for the verification of Real Time systems.
  • ObsSlice: A timed Automa Slicer based on Observers.

Service

Projects

Currently (selection):

  • Director of PIP CONICET project "Mejorando la verificación acotada usando técnicas de análisis dataflow y demostradores módulo teorías" (2012-2014).
  • Director of UBACyT project "Especificación y análisis cuantitativo del uso de la memoria dinámica con foco en la escalabilidad y usabilidad" (2012-2105).
  • Director of PICT project "Análisis cuantitativo del uso de la memoria dinámica con foco en la escalabilidad y usabilidad" (2011-2013)
  • Principal Investigator of MSR-SEIF project “Resource Usage Contracts for .NET” funded by Microsoft Research SEIF Award (2010-2011)
  • Researcher in MSR-SEIF project “Strengthening Code Contracts with Typestates” funded by Microsoft Research SEIF Award (2010-2011)
  • Researcher in ANPCyT PICT-PAE 2007 2278, “Análisis de aplicaciones y métodos de sistemas de tiempo real y embebidos”
  • Researcher in INRIA associated team ANCOME (2011-2013)

Previously (selection):

  • Director of UBACYT project "Análisis automático de programas para la inferencia de consumo de memoria dinámica" (2010-2011)
  • STIC-AMSUD TAPIOCA: Timing Analysis and Program Implementation On Complex Architectures. Jointly with LAAS-CNRS, IRIT, DAS-UFSC, Verimag, UADE (2008-2009).
  • ECOS SUD JAPIQAY Modelización y análisis de la administración automática de memoria dinámica en software embebido y de tiempo real. ECOS SUD 2007-2008. Jointly with University of Strasbourg and Verimag. Argentine (2007-2009)
  • Member of ANPCyT PICT 2005 32440: Modelos Parciales en la IngenierÌa de Software Reactivo y Embebido. 2007-2010. FONCyT.

GLAPV: Our incipient reading group in Program Analysis and Verification (currently in spanish)
GLyC: Logic and Computability Research Group
RFM: Relational Formal Methods Research Group

If you wish, you may also contact me through Facebook or Mendeley.

Undefined