Teaching
Currently:
Previously:
|
Research
Current researh interest:
- Program analysis (in particular):
- Static analysis aimed at program verification of Java like programs.
- Program understanding.
- Resource analysis: Dynamic memory requirements.
- Real-time systems: modelcheking, abstractions.
Our researh group:
-
LAFHIS Tools and Fundations for Software Engineering Lab at UBA.
My publications:
My PhD Thesis:
Parametric specifications of
dynamic memory utilization,
advisors:
Victor Braberman (DC-FCEN-UBA)
and Sergio Yovine (Verimag-CNRS)
|
Software
Find more at Tools at:
LAFHIS
-
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.
-
JConsume
: An automatic memory consumption analyzer for Java (not yet available for download).
-
Resource Contracts.NET
: An extenstion of Code Contracts to specify and verify memory consumption constraints in .NET programs.
-
BudaPest
: An automated software verifier.
-
JScoper
: An Eclipse plug-in that assist transalation of Java applications to Java Real Time ones.
-
VInTime
: A tool suite for the verification of Real Time systems.
-
ObsSlice
: A timed Automa Slicer based on Observers.
|
Projects
Currently:
- 2007-2010: ANPCyT PICT 2005 32440: Modelos Parciales en la Ingeniería de Software Reactivo y Embebido. 2007-2010. FONCyT.
- 2008-2009: STIC-AMSUD TAPIOCA: Timing Analysis and Program Implementation On Complex Architectures. Jointly with LAAS-CNRS, IRIT, DAS-UFSC, Verimag, UADE.
- 2007-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
Previously:
- 2006-2007: IBM Eclipse Innovation Grant 2006 “Early Bug Detection by Inferring Semantic Properties”
- 2004-2007: Teoría y Herramientas para la Construcción de Software Crítico.
- 2005-2006: Plugging the VinTiME Tool Suite for Verification and Validation of Real-Time and Embedded Systems into Eclipse (IBM Eclipse Innovation Award)
- 2005: SetPoint: An Aspect Oriented Framework Based on Semantic Pointcuts (Microsoft Research Phoenix Award).
- 2004: Seamlessly migrating Java applications to Java RealTime with Eclipse in teaching, research and development environments (IBM Innovations Grants)
- 2003-2004: TraceIt!: Event Trace Generator for Distributed Embedded Real-Time Applications (Microsoft Research Embbeded RFP).
- 2004: Una Herramienta para el Análisis y Síntesis de código para sistemas embebidos o críticos (Jornadas IDS).
- 2003: RTNL Expresso. Java pour l’embarqué. Laboratoire Verimag. France.
- 2000-2002: UBACYT EX156: Verificación automática de sistemas temporizados.
|
Links
|
