Description du sujet de thèse

The ANR project BLaSST targets bridging combinatorial and symbolic techniques in automatic theorem prov- ing, in particular for proof obligations generated from B models. Work will be carried out on SAT-based techniques as well as on more expressive SMT formalisms. In both cases encoding techniques, optimized resolution techniques, model generation, and lemma suggestion will be considered. Combining both lines of work, the expected scientific impact is a substantially higher degree of automation of solvers for expressive input languages by leveraging higher-order reasoning and enumerative instantiations over finite domains. The effectiveness of the techniques developed in the project will be quantified by applying them to benchmark sets provided by the industrial partner. The industrial impact of BLaSST will be a higher productivity of proof engineers.

BLaSST brings together academic experts in automated reasoning techniques (CRIL, INRIA and Université de Liège) and an industrial company (CLEARSY) leader in formal methods for a 4-year long effort that aims to provide a breakthrough in the formal verification applied to software design.

The main aim of this PhD position is to take advantage of SAT technologies to address different reasoning tasks for formal developments of software, in particular in approaches such as the B method. Indeed, this thesis will focus on developing and optimizing SAT-based encodings and techniques to achieve the following objectives:

Develop different SAT-based encodings for generating counter-examples of proof obligations.
Develop a method for building proof suggestions in connection with the proposed SAT-encodings to help showing proof obligations.
Develop a method for identifying missing premises to establish validity.
The research will be carried out in strong relationship with our industrial partner CLEARSY.

Applicant profile

We are looking for a PhD candidate with a master degree (or equivalent) in computer science with a background in logic. Prior knowledge in automated reasoning or formal methods (TLA+, B, Z or Alloy for instance) is a plus. The candidate should master one mainstream programming language such as C, C++ or Java.

Contexte de travail

The thesis will take place in Lens, within CRIL laboratory (http://www.cril.fr/). This work is part of the ANR PRCE project BLaSST. The candidate will cooperate with the other members of the consortium: INRIA Nancy, Liege University and CLEARSY.