Diego Garbervetsky

Dr. Diego Garbervetsky

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


Dr. Diego Garbervetsky

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. I am also Director of the Institute of Research in Computer Sciences(ICC).

I work on static analysis techniques aimed at 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


  • We are hiring! Please contact me for PhD and Posdoc opportunities.


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)



CurrentlyParadigmas de Lenguajes de Programación

Previously: Algoritmos y Estructuras de Datos 1Automatic Software Validation and Verification, Automatic Program Analysis, Ingeniería de Software 2Organizacion del Computador 1 (verano).

Phd Students

Former Phd Students


Former Postdocs

Undergraduate Students (simil to MSc thesis)

Previous students (link to their thesis):

Service (last 5 years)


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.


  • 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)

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