In (not so) short ...
My main research interest lies in formal methods in software engineering, especially in software verification and validation. Generally speaking, Software Engineering is about methodologies, models, techniques and tools for building software systems. In this area, the benefits of formal methods are well-known, even if currently formal methods have only gained acceptance in specific domains, with high requirements on safety or security. Besides providing a scientific background for software engineering, they support well-foundedness of the techniques and models, non-ambiguous design artifacts (specifications, models or representations), and they complement empirical approaches. They enable automated support for most activities concerned with software construction: specification (finding flaws or incompleteness), design (refinement techniques), programming (code generation from a model), validation and verification activities (testing, proving, model checking).
Research: My current work focuses on automatic generation of test cases from specifications and more precisely structural statistical testing. For simplicity, the issues are described here in terms of unit program testing, but the concern is more general.
Classical statistical program testing, i.e. automatic generation of test cases according to a probability distribution over the input domain, is a well-known method for generating test inputs. Some of its benefits are an easy generation of large test sets and a way to test the future behaviour of the program according to an expected input distribution: when the latter is known, by reflecting that "operationnal" distribution in the probability distribution used for the drawing, the (expected) most frequent uses of the program will be tested most. The associated drawback is a weak coverage of rare cases, their associated input values being under-represented in the test set. Hence, these methods have to be augmented with additional strategies for dealing with rare cases (boundary testing for instance). As an alternative, "coverage-based" statistical methods have been proposed where the drawing of test cases is designed for maximizing the probability of rare cases to be covered, although actual input values are still drawn randomly. The idea is to compute (automatically) the probability distribution to be used for the drawing to guarantee a fair exposition to test of all the parts of the program. With respect to a uniform distribution, the resulting distribution is biased towards the satisfaction of a given coverage criterion by the generated test cases.
We use results on combinatorial structures, especially some
efficient algorithms for random drawing of paths, to automate coverage-based
statistical testing from
various graphs representations (here the control flow graph of a
piece of code, but also UML-like state machine models for instance). Once
paths have been generated, we are faced to the (undecidable) problem of
knowing if there exist input values for executing exactly these paths.
come from compiler construction, program annotation,
abstract interpretation and
symbolic evaluation, combinatorial structures, and constraint-solving
(for deciding if a path corresponds to an real execution path), etc.
Some research issues are: computing the "best" combinatorial
structures or monitoring the drawing in order to avoid the selection of unexecutable paths, efficient use of constraint-solvers for finding input values for executing a given path, adequate representation of coverage criterion besides the ones stated in terms of paths.
Pushing ideas in practice is done through the design of the next version of the Auguste prototype, initially developed by Sandrine-Dominique Gouraud, for the structural statistical testing of C programs.
Teaching: Since 1982 I have taught numerous courses
at various levels,
among which: Software engineering (formal methods, UML, OCL, Testing,
Programming languages (Java, C, Ada, Lisp, SML, SmallTalk, Pascal),
Algorithmics and Data Structures, Foundations of
Object-Oriented Design, Design Patterns,
Compiler construction, Formal Language Theory, Complexity and Calculability,
Basics of operating systems.
See the (future) dedicated page for information about recent teaching and related documents.
Managerial involvement: [Sept. 2004 - Nov. 2008]:
Vice-Président Enseignement, Département
d'Informatique, Faculté des Sciences d'Orsay, Université
Overall management of the various curriculum of
the department (in cooperation with their heads) and of the
colleagues (teaching assignments for instance). Acting as the
main interface with the Faculty administration and with the department head
for any topic related to teaching.
See the (future) dedicated page for further information and past managerial activities.