Home

Research conducted in the LMV team aims at improving the quality of computer systems through the use of formal methods. Our work focus on the study of behavioral properties of complex systems described by means of programming languages, rewriting systems and partial orders. The design of approximations suitable for the analysis of such systems constitute the backbone of our team. The Coq Proof Assistant is increasingly used as a programming language as well as a validation tool in our work.

Programming languages

Our research in the field of programming languages focus on the definition of semantic property of programs and on the design of analysis tool enforcing such property. On the basis of these elements we also work on the study of new programming constructs, in particular in the field of parallel programming which occupies a central place in this activity. For example, we are involved in the development of the SyDPaCC library and in the GIRAFON project.

Rewriting systems

Our research in the field of rewriting systems focus of the study of various rewriting strategies for which we define proper termination and conflunece criterion. In particular, we consider rewriting systems based on words and tree language constraints (context-sensitive rewriting, prefix constrained rewriting, controlled rewriting).

LMV members participate to the following working groups: LTP and LaHMA (GDR-GPL), Verification (GDR-IM) and MFS (GDR-Sécurité).