# Proposition de POM, équipe CASH, LIP (Lyon7)
Titre : Program Analysis in Practise : Design and programmation of a
C static Analyser
**Advisor:** Laure Gonnord
**Co-advisor:** Julien Braine, PhD student
**Location:** Laboratoire de l'Informatique du Parallélisme (LIP), École Normale Supérieure de Lyon, France.
Please feel free to contact us for any detail, using [POM] as subject:
laure.gonnord@ens-lyon.fr, julien.braine@ens-lyon.fr
# Context
The context of the project is the Phd thesis of Julien Braine, which
designs new algorithms to prove array properties of a given
program. In the fundamental paper of his thesis ([1]) we were for
instance able to prove that a sort algorithm
actually sorts. An implementation is available on github ([2])
For the moment, our analyzer only takes as input a subset of the java
language, which makes it hard to use/test it extensively.
The goal of this internship is to be able to use a large subset of the
C language as input of the analyser.
# Objectives
The expected outcomes of the internship are:
- A refinement of the current specification of what the frontend should be
able to do, in collaboration with Julien Braine.
- A first proposition of the code design inside one known static
analyzer that most probably will be FramaC
- A code infrastructure : makefiles, unit tests, git, ... based on what already
exists.
- A first implementation and documentation (in Ocaml)
This proposal is very flexible, and may evolve as:
- a more theoretical study, for instance of how to
- a more mature tool :-)
A group of 2 students is an option.
# REFS
[1] https://hal.archives-ouvertes.fr/hal-01206882v3
[2] https://github.com/vaphor
[3] https://frama-c.com/index.html