Academic Homepage
*
Vincent Hugot
vincent.hugot@insa-cvl.fr
|
Contents
1 General Information
I am
an
Associate Professor of Computer Science
in the SDS team of the LIFO,
teaching at the INSA CVL in Bourges.
My research interests fall mainly within the perimeter of
“formal verification”, and include various aspects of automata
and transducers theory, term rewriting, formal logic,
and their applications.
Starting on April 15th, I supervise the Ph.D. thesis of
Amine Rifi, Towards Formal Semantics and Proven Compliance
of Business Workflows Processing Personal Data.
It is directed by Sabine Frittella.
I supervised the CIFRE
Ph.D. thesis of
Adrien Jousse,
defended on December 13, 2022,
on the cybersecurity of automotive networks.
The industrial partner for this
thesis
was the automotive supplier Valeo, where
Benjamin Venelle
supervised.
It was
directed by Christian Toinard.
I am head of “option 4AS”
(Architecture, Administration, Audit, and Security Analysis) since 2021.
1.1 Past Affiliations and Activities
1.1.1 Inria Links, Lille, 2013–2017
I have been a member of the Inria team Links (formerly Mostrare), under the direction of
Joachim Niehren, from October 2013 to August 2017, successively
as a post-doctoral fellow, research engineer, and
Temporary Research and Teaching Attaché (ATER), teaching at Lille 1. I worked within
the ANR CoLiS.
1.1.2 University of Franche-Comté, VESONTIO, 2011–2013
I received my Ph.D. in Computer Science in 2013 from the University of Franche-Comté, working in the
VESONTIO team of the
DISC/LIFC department of the
CNRS research institute
FEMTO-ST (UMR 6174);
I was also a member of
the Inria/CASSIS team, and
my Ph.D. was financed by the
Inria and the
Direction Générale de l’Armement
(DGA).
Thesis title: Tree Automata, Approximations, and Constraints for Verification
— Tree (Not Quite) Regular Model-Checking.
Supervised by: Prs.
Kouchnarenko
and Héam.
The manuscript can be downloaded below.
1.2 Publications and Supervisions
See also DBLP and
SmartHal.
1.2.1 Supervised Ph.D. Thesis
Protection obligatoire vérifiée au regard des
objectifs safety du secteur automobile
co-authors:
A. Jousse, C. Toinard, B. Venelle
Supervised Ph.D. thesis — Defended by Adrien Jousse on Dec 13, 2022
1.2.2 Published Papers
Handling Reachability Analysis by SAT-Solving
co-authors:
Y. Boichut, A. Boiret
International Conference CIAA 2024 — September 2024
A safe dynamic access control providing mandatory automotive cybersecurity
co-authors:
A. Jousse, C. Toinard, B. Venelle
International Conference CSCI — 2021
oMAC : Open Model for Automotive Cybersecurity
co-authors:
A. Jousse, C. Toinard, B. Venelle
International Conference (Automotive Cyber Security) ESCAR — 2019
-
Equivalence of Symbolic Tree Transducers
co-authors:
A. Boiret, J. Niehren
Springer LNCS – International Conference DLT’17 — August 2017
Automata for Unordered Trees
co-authors:
A. Boiret, J. Niehren, R. Treinen
Elsevier — International Journal
Information & Computation — April 2017
The Emptiness Problem for Tree Automata with at Least One
Disequality Constraint is NP-hard
co-authors:
P.C. Héam, O. Kouchnarenko
Elsevier — International Journal
Information Processing Letters.
— February 2017
Logics for Unordered Trees with Data Constraints on Siblings
co-authors:
A. Boiret, J. Niehren, R. Treinen
Springer LNCS – International Conference LATA’15 — March 2015
Deterministic Automata for Unordered Trees
co-authors:
A. Boiret, J. Niehren, R. Treinen
EPTCS – International Symposium GandALF’14 — July 2014
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.
From Linear Temporal Logic Properties to Rewrite Propositions
co-authors:
P.C. Héam, O. Kouchnarenko
Springer LNCS – International Conference IJCAR’12 (Long Paper) — Jan 2012
Corresponding slides.
-
(internal) Presented to the VESONTIO team
on May 30, 2013 in Besançon, France.
- Presented at the
GPL-GRD FORWAL meeting,
on Wednesday, May 23 2012, in Paris, France.
- Presented at IJCAR’12 in Manchester, Great Britain, on
June 26th, 2012.
- Presented to the DGA
in Bruz, France, on September 28, 2012.
- Erratum: the translation rule (⊥) is obviously erroneous in this version.
Refer to the updated paper.
On Positive TAGED with a Bounded Number of Constraints
co-authors:
P.C. Héam, O. Kouchnarenko
Springer LNCS – International Conference CIAA’12 (Short Paper) — March 2012
Corresponding slides.
-
Extended version presented at the
GPL-GRD FORWAL meeting,
on Thursday, July 4, in Paris, France.
- (internal) Presented to the VESONTIO team on May 2, 2013 in Besançon, France.
- Presented to the GDR-GPL-CIEL-AFADL FORWAL
meeting in Nancy, France, on April 3rd, 2013.
- Presented at CIAA’12 in Porto, Portugal on July 20, 2012.
Loops and Overloops for Tree Walking Automata
co-authors:
P.C. Héam, O. Kouchnarenko
Springer 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.
- (internal) 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.
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.
1.2.3 Current Drafts (Works in progress / submission / revisions)
Symbolic Register Tree Transducers
with Symbolic Register Lookahead
co-authors:
A. Boiret
Conference and/or Journal paper — work in progress
1.2.4 Thesis, Research Reports, and Such
Tree Automata, Approximations, and Constraints for Verification — Tree (Not Quite) Regular Model-Checking
co-authors:
supervisors: P.C. Héam, O. Kouchnarenko
Ph.D. Thesis — Sept 27, 2013
Corresponding slides.
-
Defended on September 27, 2013,
in Besançon, France.
Random Generation of Positive TAGEDs wrt. the Emptiness Problem
co-authors:
P.C. Héam, O. Kouchnarenko
INRIA Research Report — November 2010
Corresponding slides.
Algorithms for Tree Automata with Constraints
co-authors:
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.
2 Miscellaneous Odds and Ends
- 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 (≈ 850)
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). - My Python implementation of nondeterministic finite automata
This was not originally intended for public consumption at all, but
I found it useful enough for pedagogical and research prototyping
purposes.It consists in a very naive implementation of NFA and most algorithms
thereon (determinisation, minimisation, language enumeration,
morphisms, various kinds of products including parameterized synchronised product, CTL model-checking,...), graphviz/dot-based PDF visualisation,
generation of LaTeX figures, conversion of regular expressions to automata,...
Not yet available but somewhat planned: tree automata, term rewriting, LTL/CTL* model-checking.
Given that what little documentation exists is interspersed with my
teaching materials, and that it’s not coded with readability in mind,
I don’t really expect it to be of much use to anyone who
did not write it — I didn’t even bother giving it a name — but here it is.
This document was translated from LATEX by
HEVEA.