Image

Jesus Mauricio Chimento

Department of Software and Computer Systems
KTH University of Technology

About me

About me

I'm Jesús Mauricio Chimento, PhD in computer science. I am part of the department of Software and Computer Systems, where I am doing a PostDoc working with David Broman working in a project regarding full-stack verification of programs synthesized from timed automata. This project is financially supported by the Wallenberg AI, Autonomous Systems and Software Program (WASP).
My research interests focus on studying Formal Methods, Certified Programming and Functional Programming. Regarding Formal Methods, I am keen on studying Program Specification and Program Verification, in particular Theorem Proving and Runtime Verification.

Education

Education

You can click on the titles for more details.

experience

experience

I have worked in the following research projects:

StaRVOOrS

* Period: 2013 - 2016
* WWW


VirtualCert

* Period: 2011 - 2013
* WWW



In addition, I have done the two interships listed below. You can click on their titles to see more details about them.

  • VirtualCert Project                                                                                               2012

    • * Place: Instituto de Computación. Universidad de la República, Uruguay.
    • * Supervisors: Carlos Luna and Gustavo Betarte
    • * Date: December 3, 2012 - December 18, 2012
    • * Summary: The internship consisted on proving the validity of part of the state invariance under (system) actions execution property.
  • INRIA, International interships program                                                   2010

    • * Place: INRIA - Loria Nancy, Francia
    • * Date: April 6, 2010 - July 3, 2010
    • * Project: Model-Checking Distributed Algorithms with Pluscal 2.0
    • * Group: Algorille
    • * Supervisors: Stephan Merz and Martin Quinson
    • * Summary: The internship consisted on checking the effectiveness of using Pluscal 2.0 when specifying distributed algorithms, testing the Pluscal 2.0 compiler andfixing the spotted bugs which were found during the testing stage.

teaching

teaching

I have worked as teaching assistant in the universities listed below. You can click on their names to see the list of courses I have taught.

Publications

Publications

Testing Meets Static and Runtime Verification


J. M. Chimento, W. Ahrendt, and G. Schneider.
FormaliSE'18. June 02, 2018. Pages 30-39. ACM.

Bibtex PDF Pre-print PDF

Verifying data- and control-oriented properties combining static and runtime verification: theory and tools


W. Ahrendt, J. M. Chimento, G. Pace, and G. Schneider.
Formal Methods in System Design. 04 April 2017. Springer.

Bibtex PDF Pre-print PDF

StaRVOORS: A Tool for Combined Static and Runtime Verification of Java


J. M. Chimento, W. Ahrendt, G. Pace, and G. Schneider.
Runtime Verification 2015 (RV'15). Volume 9333 of LNCS, pages 297-305, Vienna, Austria, September 23-25 2015. Springer

Bibtex PDF Pre-print PDF

A Specification Language for Static and Runtime Verification of Data and Control Properties


W. Ahrendt, J. M. Chimento, G. Pace, and G. Schneider.
Formal Methods 2015 (FM'15), 20th International Symposium on Formal Methods. Volume 9109 of LNCS, pages 108-125, Oslo, Norway, June 24-26 2015. Springer.

Bibtex PDF Pre-print PDF

Formally verified implementation of an idealized model of virtualization


Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Jesús Mauricio Chimento and Carlos Luna.
19th International Conference on Types for Proofs and Programs (TYPES 2013).

PDF

contact

contact

phone

Office phone no phone at the moment