Giorgino Mathieu   Status : Doctorant   Service / Team :  Assistance à la Certification des Applications DIstribuées et Embarquées   Contact : FirstName DOT FamilyName AT irit.fr   Localization : IRIT1 / Level 4, Office: 417   Phone : +33 (0)5 61 55 8456   PGP : public key   Publications :

 

Research

 Publications

  2010

• BDDs verified in a proof assistant (Preliminary report)

• Verification of the Schorr-Waite algorithm - From trees to graphs

  2009

• Génération de programmes efficaces et vérifiés

  2008

• Vérification de structures de pointeurs

  2006

• Towards a Formalisation of Graph Transformations in Proof Assistants

 Research Topics

• Software safety

• Model engineering

I'm interested in generation of programs with pointers, along with reasoning about algorithms using pointers. Our approach is to add pointers to tree data structures.

 

 Current Research Activities

Phd student since 09/2008 on the subject:

My advisors are Martin Strecker and Ralph Matthes.

 

 Research Experience

• 03-09/2008: ENSEEIHT 3^rd year internship / MA SIGL

  At IRIT in the ACADIE team.

  Report

• Summer 2007: ENSEEIHT 2^nd year internship

  At the University of Leicester in Computer Science and Mathematics department for the ACADIE team of IRIT.

• Summer 2006: ENSEEIHT 1^st year internship

  At IRIT in the ACADIE team.

 

 

 

Teaching

Teacher assistant in the "Paul Sabatier" University.

• 2008-2009

  • (practical) L1.Computer science - Introduction to Computer-Science: Initiation to the Caml Language.
  • (practical) L1.* - C2i: Preparation to C2i certification level 1.
  • (practical) L2.Maths/Mechanics - C language.
  • (practical) L3.Computer Science - Prolog language.

  Assisting a teacher

• 2009-2010

  • (practical) L1.Computer Science - Introduction to Computer-Science: Initiation to the Caml Language.
  • (practical) L3.Computer Science - Algorithms, datatypes and proofs.
  • (practical) M1.Computer Science - Languages specification and translation.
  • (practical) 1st year ENSEEIHT, Computer Science - Object technologies and Software engineering.
  • (practical) 2nd year ENSEEIHT, Telecom and networks - Object Languages: Java and UML.

• 2010-2011

  • (practical) L3.Computer Science - Algorithms, datatypes and proofs.
  • (practical) M1.Computer Science - Languages specification and translation.
  • (practical) 1st year ENSEEIHT, Computer Science - Object technologies and Software engineering.
  • (practical) 2nd year ENSEEIHT, Telecom and networks - Object Languages: Java and UML.