The Coq mailing list

[Stephan Merz <Stephan.Merz AT loria.fr>]

Post-doctoral position in formal verification of computer systems

LORIA -- QSL group, Nancy, France

http://qsl.loria.fr/


Applications are invited for a one-year post-doctoral research position 
available in the QSL group (qualité et sûreté des logiciels, quality and 
safety of software-intensive systems). Candidates are expected to have a 
strong background in formal methods and/or deductive or verification tools.

The goal of our research is to support the application of formal methods 
of system development in practice by providing tools and interfaces that 
combine a high degree of automation with facilities for user interaction 
at a meaningful level of abstraction. More specifically, we are working 
on a framework (language and tools) that allows for the combination of 
deductive software such as interactive proof assistants, model checkers, 
and decision procedures for various first-order theories, and to make 
this combination produce proofs that can be certified by an independent 
proof checker. A tangible outcome should be the certification of parts 
of the FlexRay suite of protocols (http://www.flexray-group.com/). We 
are currently working with the Isabelle proof assistant 
(http://isabelle.in.tum.de/) as our integration framework and use 
external tools such as SAT solvers, CVC Lite, ICS, and haRVey.

The successful candidate will work in the QSL group at LORIA 
(http://www.loria.fr/), one of the French centers of excellence in 
computer science. The QSL group includes several research teams working 
on the use of formal methods in computer science.

Applicants should submit a Curriculum Vitae, a statement of research, 
and names of references. Applications should be received by September 5, 
2005, although the search will continue until an appropriate candidate 
has been identified.

Informal inquiries about the position should be directed to

Jean-Yves Marion 
(Jean-Yves.Marion AT loria.fr)
   or
Stephan Merz 
(Stephan.Merz AT loria.fr)