Diego Garbervetsky
Dr. Diego Garbervetsky
FTA Professor @ LaFHIS, DC, FCEyN, Universidad de Buenos Aires
About
![]() |
I am an Associate Professor at the Computer Science Department, School of Sciences, University of Buenos Aires. I am also a Researcher at the ICC/CONICET. Currently I am also vice-Director of the Institute of Research in Computer Sciences(ICC). I am interested in automatic program analysis. I am currently working in static analysis techniques aimed at resource usage analysis of Java-like programs and Smart Contracts, automated program verification, program understanding and validation. Phone: +54 11 5285-7482, email: diegog@dc.uba.ar Twitter: @diegarber |
News
- We are hiring! Please contact me for PhD and Posdoc opportunities.
Research
Current researh interests are in Program analysis (in particular):
- Program understanding.
- Testing and verification of program featuring rich protocols
- Static analysis aimed at program verification of Java like programs.
- Automatic symbolic resource analysis (gas consumption, dynamic memory, energy, etc)
Publications
- Find me on: Google Scholar, ResearchGate, Microsoft Academic Search, DBLP, ACM.
- Most PDFs files are here
My PhD Thesis: Parametric specifications of dynamic memory utilization, advisors: Victor Braberman (DC-FCEN-UBA) and Sergio Yovine (Verimag-CNRS/CONICET)
Teaching
Currently: Paradigmas de Lenguajes de Programación
Previously: Algoritmos y Estructuras de Datos 1, Automatic Software Validation and Verification, Automatic Program Analysis, Ingeniería de Software 2, Organizacion del Computador 1 (verano).
Phd Students
Former Phd Students
- Guido Chari (now Postdoc with Jan Vitek at Czech Technical University)
- Rodrigo Castaño (currently at Microsoft)
- Edgardo Zoppi
- Guido de Caso (currently at Dialpad)
Postdocs
- Rodrigo Castaño (currently at Microsoft)
Former Postdocs
- Sven Stork now at Duolingo
Undergraduate Students (simil to MSc thesis)
Some offered thesis topics: Enablabledness models, Resource Analysis, Modular Verification,Bounded Verification
Previous students (link to their thesis):
- 2021: Dardo Marasca (co-advisor Guido Chari), Francisco Curdi (co-advisor Edgardo Zoppi)
- 2019: Vera Bogdanich, Manuel Carrasco (co-advisor Juan Manuel Martinez Caamaño)
- 2018: Rodrigo Campos Catelin (co-advisor Jens Gustedt)
- 2017: Patricio Palladino
- 2016: Leandro Lera Romero, Ivan Postolski (co-advisor Victor Braberman)
- 2015: Sebastian Lamelas Marcote (co-advisor Martin Montperrus)
- 2013: Fernando Paulovsky (co-advisor Esteban Pavese), Juan Manuel Martinez Caamaño (co-advisor Philippe Clauss)
- 2012: Edgardo Zoppi (co-advisor G. de Caso), Marcos Chicote (co-advisor J.P. Galeotti)
- 2011: Bruno Cuervo Parino (co-advisor J.P. Galeotti), Jonathan Tapicer (co-advisor M. Rouaux)
- 2010: Pablo Bendersky (co-advisor J.P. Galeotti), Ariel Neisen (co-advisor D. Gorin), Fernando Benavidez (co-advisor D. Gorin), Alexis Tchach (co-advisor G. de Caso), Matias Grumberg and Gaston Krasny (co-advisor M. Rouaux)
- 2009: Martin Rouaux (co-advisor S. Yovine), Alejandro Taboada (co-advisor S. Yovine)
- 2007: Guido de Caso (co-advisor D. Gorin)
- 2006: Diego Piemonte, Federico Fernandez (co-advisor F. Bonomo)
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.
- Consume.Net: A compositional analysis for inferring heap memory consumption in .Net Programs.
- Resource Contracts.NET: An extenstion of Code Contracts to specify and verify memory consumption constraints in .NET programs.
- 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.
Analysis of .NET programs
- analysis-net: A library to perform control flow and dataflow analysis on .Net programs (by Edgardo Zoppi)
Service (last 5 years)
- Program Committee at FMics 2021
- Program Committee at WosCA 2020
- Program Committee at ICSE 2021
- Program Committee at FSE 2020
- Program Committee at The Art, Science, and Engineering of Programming 2020
- Program Committee at NIER Track at ICSE 2020
- Program Committee at ICSE 2019
- Program Committee at VEE 2018
- Program Committee at FM 2018
- Local arrangements chair at ICPC 2017
- Program Committee at SEIP 2017 @ICSE2017
- Program Committee for the Workshop Proposals @ICSE2017
- Program co-chair of the 3rd ICSE warm up symposium
- Program co-chair at ASSE 2016
- Program Committee at FM 2016
- Program Committee at FM 2015
- Reviewers Committee at ICSE 2015
- Program Committee at ISMM 2014
- Program Committee at ASE 2014
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.
Links
- 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.