The Coq mailing list

[Laurent Th�ry <Laurent.Thery AT inria.fr>]

Hi,

this may be of some interest:

===============================================================================

Engineer position in Satisfiability Modulo Theories (SMT) solving

An engineer position is available in the VeriDis team 
(http://veridis.loria.fr/) of INRIA Nancy (http://www.inria.fr), France.

CONTEXT: INRIA, the French national institute for research in computer 
science and control, is dedicated to fundamental and applied research in 
information and communication science and technology. The VeriDis team 
aims to exploit and further develop the advances and integration of 
interactive and automated theorem proving applied to the area of 
concurrent and distributed systems.

MISSIONS: the veriT solver (http://www.veriT-solver.org) is an SMT 
solver developed jointly at UFRN in Brazil, and at INRIA in the VeriDis 
team. It checks the satisfiability of large logic formulas. The engineer 
will support design, implementation and evaluation of veriT. The goal of 
the new implementations is to extend the expressivity, the efficiency, 
and the integrability of the tool. The veriT development team will be 
represented in the major international events of the domain, and in 
particular, at the annual competition of SMT solvers.

REQUIREMENTS: the candidate should have
* proven skills and strong interest in programming and algorithms
* knowledge of the C language
* knowledge of logic (propositional, predicate)
* other expertise that is not required but appreciated: proof 
assistants, first-order or SMT provers, higher-order logic, 
verification, python

DEADLINE: June 1st 2011 - Target starting date: October 2011.

ELIGIBILITY CRITERIA: Candidates are required to have obtained recently 
(that is, since less than a year, and before the starting date) a master 
-- or equivalent -- degree in Computer Science or Computer Engineering.

SALARY: approx. 2000 € (2500€ gross) monthly. This is enough to live 
very comfortably in Nancy, France.

DURATION: one year, extendable to a second year.

APPLICATION: applications accompanied by a CV and a letter of motivation 
should be sent as soon as possible to Pascal.Fontaine AT loria.fr .

==========================================================================