Members

• HEAM Pierre-Cyrille, Assistant Professor, Laboratoire d'Informatique de Franche Comté
  
  
  Pierre-Cyrille HEAM has done his PhD at Université Paris 7, LIAFA, on algorithmic problems related to finite automata. He joined the LIFC group in 2002 to work on automata based techniques dedicated to reachability analysis. He is now working on regular model checking techniques using approximations.
  
  
  Participation in research projects
  • Project INTAS 1224, 2002
  • Project RNTL PROUVE, ended in Mai 06
  • Project ACI SATIN, ends in Jully 07
  • Project IST-AVISPA, ended in June 05
  
  PhD Students
  
  • R. Courbis to be defended in 2010.
  
  
• KOUCHNARENKO Olga, Professor, Laboratoire d'Informatique de Franche-Comté (LIFC)
  
  Olga Kouchnarenko obtained a PhD in Computer Science from the University Grenoble I, France, in 1997; supervisors Ph. Schnoebelen and V. Sokolov. She got an habilitation (HDR) in Computer Science from the University of Franche-Comté, France, in 2004. Since September 2006, she is Professor at the University of Franche-Comté, leader of the TFC (later VESONTIO) team at the LIFC concerned with specification, verification and testing for software validation.
  
  Her main research interests include software specification and verification. She has also worked on applying abstraction/refinement based techniques to component-based systems. She is/has been involved in several national and european projects, in particular European Project IST AVISPA (2003-2005), French ACI projects ”Information Security” GECCOO (2003-2006),  SATIN (2004-2007), COPS (2006-2008) and TACOS (2007-2009).
  She is currently acting as vice-head of the CASSIS project/team at LORIA, is responsible for the Computer Science Licence at the University of Franche-Comté.
  
  PhD Students
  
• R. Courbis to be defended in 2010.
  
  
• COURBIS Roméo, PhD student, Laboratoire d'Informatique de Franche-Comté (LIFC) and INRIA/Cassis
  
  Supervisors: P.-C.Héam and O. Kouchnarenko
  
  Topics: Rewriting Approximations, Property Guided Abstraction Refinement
  and Verification
  
  
  Roméo Courbis is working on the improvement of the approximation-based
  verification technique for Java bytecode analysis. Its principal subjects
  are abstraction refinement and property-guided verification. They
  
  address the questions of having conclusive analysis to make the
  approximation-based technique more (or fully) automatic.
  
  
  The abstraction refinement is a technique which allows backward analysis
  and automatic modification of abstraction function according to
  counter-examples. So, the approximation-based verification technique may
  lead to more conclusive analysis.
  
  The property guided-verification includes two main tasks. The first one is
  the automatic generation of abstraction function guided by properties
  
  to be ensured. The purpose of this work consists in having conclusive
  
  analysis without the help of an expert for the abstraction function
  definition. The second task consists in developing an efficient technique
  
  for verifying properties expressed for example by temporal logic formulae.
  
  
• Aloïs Dreyfus, Engineer at LIFC Besançon. Joined the project in October 2008 for 12 months.
  

• BOICHUT Yohan, was PhD student at LIFC, now Assistant Professor at Université d'Orléans and LIFO.
  
  

• Pierre-Etienne Moreau, researcher at LORIA/INRIA Lorraine in the Pareo team.
  
  His main research activity consists in conceiving tools and languages that help to write complex applications, by decreasing the development time and increasing the confidence. In this direction, he has developed during his thesis a compiler for the ELAN language. Since 2001, he is managing the development of the Tom system, which allows to integrate the notions of equational matching, rule based programming, and strategic programming in languages like Java.. The main applications of Tom are the implementation of compilers, program analysis and transformation tools, as well as automatic provers.
  
  
  PhD students:
• E. Balland, PhD started in September 2005
• C. Tavares, PhD started in September 2007
• T. Bourdier, PhD started in March 2008
  
  Participation in other projects:
  • ACI Modulogic, ended in June 2006
  • RNTL Manifico, ended in September 2006
  
  
  
• Emilie Balland, PhD student at LORIA/INRIA Lorraine in the Pareo team.
  
  Thesis subject: Design of a dedicated language for program
  transformation and analysis
  
  The purpose of this thesis was to turn the concepts of term and
  term-graph rewriting into new programming paradigms adapted to program
  transformation and analysis.  Instead of developing a new standalone
  dedicated language, the chosen approach was to integrate new language
  constructs in generalist languages like Java. The Tom language provides
  a higher level language piggybacked on top of Java for describing tree
  traversals and transformations.  All the contributions of this thesis
  have been integrated in this embedded dedicated language.
  
  
  

• Thomas JENSEN holds a Cand. scient. in Computing and Mathematics from the Univ. of Copenhagen, a PhD from Imperial College London and a “Habilitation à diriger des recherches” from Université Rennes 1. In 1993 he joined the CNRS where he is “Directeur de recherche”, affiliated with the IRISA laboratory in Rennes. Since 1999, he is leader of the Lande project concerned with semantics-based techniques for software validation. His research interests concern static analysis, abstract interpretation and software security with an emphasis on security of embedded Java devices such as Java Cards and Java on mobile telephones. He has participated in the FET/Open project "Secsafe" on smart card security and is involved in the FET/IP "Mobius" on software certificates through program analysis. He is currently acting as vice-président of the Scientific Board (“Comité des projets”) at IRISA, is responsible for the French summer school for young researchers in Programming and is member of the evaluation board of INRIA.
  
  
• Thomas GENET, Associate Professor at IRISA/University of Rennes, Full researcher position at IRISA from 2006 to 2008
  
  His main research interests are verification, automated deduction, security. After a PhD on automated deduction and term rewriting in Claude and Hélène Kirchner Group in LORIA/Nancy (France), he studied cryptographic protocol verification during a one year postdoctoral position in France Telecom R&D. Then, he moved to Thomas Jensen's Group in IRISA/Rennes and he is now working on interactions between automated deduction techniques, abstract interpretation and static analysis.
  
  During his PhD, he proposed a verification technique based on regular over approximation of sets of reachable terms in term rewriting systems. He is also the main developer of the Timbuk tool (http://www.irisa.fr/lande/genet/timbuk/) which implements this technique and provides a complete library for tree automata manipulation. While in France Telecom with F. Klay, he proposed a way of verifying cryptographic protocol using approximations which is currently used in the AVISPA system [ABB⁺05]. Now at IRISA, he is part of several collaborations with Thomson for cryptographic protocol verification and with France Telecom for Java programs static analysis.
  
  PhD Students:
  • Benoît Boyer (to be defended in 2009)
  
  Participation in research projects
  • Project ACI SATIN, ended in July 07
  • Project CRC-MEFORSE between INRIA and France Telecom
  
  
  
• Vlad RUSU, Researcher at IRISA/INRIA Rennes
  
  His main line of research consists in studying the interaction between symbolic verification and testing techniques for reactive systems. He has also worked in theorem proving-based verification, specifically, making this kind of verification more automatic and applying it to real systems. He has recently become interested in applying abstraction/refinement techniques to rewriting systems - while visiting the group of Jose Meseguer at Univ. Urbana Champaign (USA) in the framework of a CNRS/Univ. Urbana Champaign cooperation.
  
  
  
• Benoît Boyer, PhD student at IRISA Rennes. Advisors: Thomas Jensen, Thomas Genet.
  
  Thesis subject: Certification of tree automata.
  
  This thesis is concerned with the certification of static analysis tools based on tree automata. Given a term rewriting system R and a tree automaton A, one of the goal of this thesis is to certify that A is a super-set of terms reachable by R. Such automata are obtained using complex tree automata completion algorithms, whose implementation may contain bugs. Certifying the completion, even if it was possible, is not relevant since those algorithm are constantly improved or optimized. However, a tool certifying the result, i.e. the completed tree automaton, is more simple to build and more long-lived.
  The idea is to formally define tree automata theory and term rewriting theory in Coq and then to automatically produce the checker using the Coq extraction mechanism. The main difficulty is to formally define such theoretical objects while keeping good performance for the extracted programs.
  
  
• Nicolas Barré, Engineer at IRISA Rennes. Joined the project for 3 monthes in 2008.
  

• Luka LEROUX, PhD student at IRISA/INRIA Rennes. Advisors: Thomas Jensen, Thomas Genet and Pierre Crégut (France Telecom). Left in 2007.
• Laurent Hubert, Engineer at IRISA Rennes. Joined the project for 3 monthes in 2008.