Jesus
Mauricio
Chimento

Software Application Developer

2021 - ongoing

Jeppesen Systems, a Boeing company. Gothenburg, Sweden

• Currently I am working as a software application developer on the Jeppesen Crew Tracking system.

High-Confidence Formal Verification of Real Cyber-Physical Systems: from Models to Machine Code

2019 - 2021

KTH University, Stockholm, Sweden

• Research project regarding full-stack verification of programs synthesized from timed automata.
• My key achievements were the implementation of a model checker for timed automata, and formally verifying that the model checker is sound.
• All this work was developed using the COQ proof assistant.

Unified Static and Runtime Verification of Object-Oriented Software

2013 - 2016

Chalmers University of Technology, Gothenburg, Sweden

• Research project regarding the combination of static and runtime verification techniques.
• I developed in Haskell a tool, called StaRVOOrS, which combines the use of the runtime verifier LARVA with the (static) deductive verifier KeY. Both verifiers target Java programs.
• I extended the APIs of the verifiers mentioned above in order to support their use within StarVOOrS, and added specific functionalities for the combined verification process. Both APIs are implemented in Java.

VirtualCert

2011 - 2013

Instituto de Computación, Montevideo, Uruguay

• Research project regarding the formalisation and verification of an idealised model of a virtualisation platform.
• My key achievement in this project was specifying and verifying the correctness of the memory management of an idealized model of a virtualization platform, in the presence of actions executed by the underlying system.
• All this work was developed using the COQ proof assistant.

Internship at the National Institute for Research in Digital Science and Technology (INRIA)

2010

INRIA, Nancy, France

• During this intership I checked the effectiveness of using the language Pluscal 2.0 for specifying distributed algorithms, tested its compiler, and fixed several bugs spotted during the testing phase.
• This compiler is implemented in Java.

Chalmers University of Technology (Sweden)

2013 - 2018

• Concurrent Programming (2016-2018)
• Formal Methods for Software Development (2017)
• Software Engineering using Formal Methods (2014-2016)
• Introduction to Functional Programming (2014-2016)
• Programming Language Technology (2015)
• Object Oriented Programming (2014)
• Testing, Debugging and Verification (2013-2017)

Universidad Nacional de Rosario (Argentina)

2006 - 2012

• Analysis of Programming Languages I (2012 - 2013)
• Course responsible for an introductory course to the CS. program (2012)
• Communications (2012)
• Formal Program Construction In Type Theory (2011-2012)
• Introduction to Computer Science (2011)
• Data Structures (2007 - 2009)
• Programming Languages Analysis II (2007 - 2010)
• Computer Architecture (2006)

Doctoral Studies

2013 - 2019

Chalmers University of Technology, Gothenburg, Sweden

• PhD degree in Computer Science
• Thesis title: Combined static and dynamic verification of object oriented software through partial proofs
• Supervised by: Wolfgang Ahrendt (main supervisor), and Gerardo Schneider

Licentiate in Computer Science

2013 - 2016

Chalmers University of Technology, Gothenburg, Sweden

• Thesis title: Unified Static and Runtime Verification of Object-Oriented Software
• Supervised by: Wolfgang Ahrendt (main supervisor), and Gerardo Schneider

Licenciatura en Ciencias de la Computación

2005 - 2012

Universidad Nacional de Rosario, Rosario, Argentina

• 5-years computer science degree + final Thesis, equivalent to a Master degree in the EU system
• Thesis Title: Memory Models Analysis in Virtualization Platforms. Formalizing a Functional Prototype of such a Platform with Cache and TLB.
  (available only in Spanish)
• Supervised by: Carlos Luna (main supervisor), and Gustavo Betarte