Academic Homepage^*
Université de Franche-Comté, DISC (LIFC)

Contents

• 1  General
• 2  Teaching
• 3  Research
  • 3.1  General information
  • 3.2  Publications and Talks
  • 3.3  Other Events and Talks
• 4  Miscellaneous Odds and Ends

1  General

I am a Ph.D. student working in the Laboratoire d’Informatique de Franche-Comté (LIFC), (now Département d’Informatique et de Systèmes Complexes (DISC), part of FEMTO-ST) as a member of its VESONTIO research team. I am also a member of the INRIA-CASSIS team.

My Ph.D. is co-financed by the Institut National de Recherche en Informatique et Automatique (INRIA) and the Direction Générale de l’Armement (DGA).

Thesis title: Approximations and Constraints: Application to the Verification of Embedded Systems.

My Curriculum Vitæ can be found here. It includes a list of publications, which is quite probably less up-to-date than the one on this page.

NOTE: two versions of this page exist:

• The full, (probably) up-to-date page which you are currently reading.
• The page embedded into the LIFC website may be found there. Currently it should just point you back here.

2  Teaching

This section keeps track of my teaching activities. Whenever relevant, the title of each module (ie. subject matter) links to its Moodle homepage, while the year links to the homepage of the whole class. Ratios of the form (n/N) indicate that the class was partitioned in N groups, n of which were assigned to me. The mention resp. indicates that I was responsible for the teaching material and exams.

• 2010–2011:
  
  Logics and Deduction     (Licence, year 2, semester 1)
  
  Classes (1/2): Propositional, first-order and temporal logics

  Lab classes (2/2), resp.: Introduction to functional programming with OCaml, and application to the manipulation of propositional formulæ

  Semester project     (Licence, year 3, semester 2)
  
  Supervision: One student project, in the Mésocentre de Calcul
• 2011–2012:
  Probably no teaching activities.

3  Research

3.1  General information

Thesis title: Approximations and Constraints: Application to the Verification of Embedded Systems.

My goal is to develop efficient techniques of automatic verification, primarily based on various strains of tree automata. In particular, I have worked with TAGED (Tree Automata with Global Equality and Disequality constraints) and TWA (Tree Walking Automata).

3.2  Publications and Talks

This section is intended to keep track of my papers and given talks. PDF versions of the papers and the related slides are provided for download whenever possible.

3.2.1  Latest Peer-Reviewed Papers (Accepted & Pending Publication)

1. Loops and Overloops for Tree Walking Automata (Extended Version)
   co-authors: P.C. Héam, O. Kouchnarenko
   Elsevier – International Journal TCS   —  December 2011 – March 2012
   Additional webpage and slides.
2. From Linear Temporal Logic Properties to Rewrite Propositions
   co-authors: P.C. Héam, O. Kouchnarenko
   LNCS – International Conference IJCAR’12 (Long Paper)   —  Jan 2012
   
   • Upcoming presentation at the GPL-GRD FORWAL reunion, on Wednesday, May 23 2012 in Paris, France.
   • To be presented in Manchester, UK sometime between June 26th and July 1st, 2012.
3. On Positive TAGED with a Bounded Number of Constraints
   co-authors: P.C. Héam, O. Kouchnarenko
   LNCS – International Conference CIAA’12 (Short Paper)   —  March 2012
   
   • To be presented in Porto, Portugal on July 17-20, 2012.

3.2.2  Published (Peer-Reviewed) Papers

1. Loops and Overloops for Tree Walking Automata
   co-authors: P.C. Héam, O. Kouchnarenko
   LNCS – International Conference CIAA’11 (Long Paper)   —  March 2011
   Additional webpage and slides.
   • Presented in detail at the INRIA ARC ACCESS meeting
     on April 5, 2011 in Lille, France.
   • Another, shorter presentation has been given to the VESONTIO team
     on July 6, 2011 in Bretonvillers, France.
   • Finally, presented at the CIAA’11 international conference
     on July 14, 2011 in Blois, France.
2. SAT Solvers for Queries over Tree Automata with Constraints
   co-authors: P.C. Héam, O. Kouchnarenko
   IEEE – International Workshop CSTVA’10   —  January – April 2010
   Corresponding slides.
   • Presented at the CSTVA’10 international workshop on April 10, 2010 in Paris, France.

3.2.3  Research Reports and Such

1. Random Generation of Positive TAGEDs wrt. the Emptiness Problem
   co-authors: P.C. Héam, O. Kouchnarenko
   INRIA Research Report   —  November 2010
   Corresponding slides.
   • Presented at the WTS’10 international workshop
     on October 11, 2010 in Nancy, France.
2. Algorithms for Tree Automata with Constraints
   supervisors: P.C. Héam, O. Kouchnarenko
   M.Sc. Thesis   —  July 2010
   Corresponding slides.
   • Presented to the LIFC on July 7, 2010 in Besançon, France.

3.3  Other Events and Talks

This section keeps track of other events I have attended and talks I have given for work-related reasons, but which do not fit in any specific category.

• Informal, impromptu talk given at the last INRIA ARC ACCESS meeting on December 16, 2011 in Nancy, France, about the general ideas of the LTL → Rewrite Proposition → TAGED semi-decision model-checking chain. See our IJCAR’12 paper for more details.
• Short, very informal talk given at the local Journée des Doctorants du LIFC 2011 on August 29, 2011 about the basic problematics of my work areas. (slides)
• I have attended the Summer School Marktoberdorf 2011: Tools for Analysis and Verification of Software Safety and Security, held in Bayrischzell, Germany, from August 2 to August 14, 2011. I have only good things to say about it ;)

4  Miscellaneous Odds and Ends

I have written a number of small programs in my spare time. Here are links to some of those which may be of interest to someone else in an academic context. All links point to topics dedicated to those programs on my personal forum, or to the program’s documentation if it is hosted elsewhere.

• qtest: Inline unit tests extractor for OCaml projects
  qtest is part of the Batteries development platform for OCaml. Batteries uses qtest to extract and run its many (≈ 800) inline unit tests. qtest is not tied to Batteries however, and can be used with OCaml projects large and small. (note: here qtest refers to version 2 only – I didn’t write v1, and it has been phased out now).
• ZapoT_EX: OCaml to L^AT_EX translation
  ZapoTeX is a pretty-printer, used to integrate nice, syntax-highlighted OCaml code, B Method specifications and Prolog code in LaTeX documents. It supersedes and improves most of the functionality of PLT_EX and DumBeX.
• Patch KeY: Export L^AT_EX logic proof
  This is a small, quick and dirty patch for the KeY prover (1.4.0), overriding the default (useless) LaTeX export mode.
• Granny (Script for Removing Left-Recursions from a Grammar)
  For those people who are far too lazy to do it by hand. Such as me. With LaTeX export mode.

Other items of potential interest — that are not programs written by me.

• Public, free MathT_EX web-service
  I host a free MathTeX server that anyone is welcome to use to add LaTeX rendering facilities (formulæ → images) to online bulletin boards (phpBB, vBulletin, IPB, Moodle forums etc), HTML emails etc, without having to install any software on their own server.

*

This page was last updated on May 14, 2012.

This document was translated from L^AT_EX by H^EV^EA.