Accueil > Liste des offres > Détail d'une offre
2022-04898 - PhD Position F/M Automated Reasoning for Set Theory
Le descriptif de l’offre ci-dessous est en Anglais

Type de contrat : CDD

Niveau de diplôme exigé : Bac + 5 ou équivalent

Fonction : Doctorant

Contexte et atouts du poste

Team
VeriDis, INRIA Nancy Grand-Est, https://team.inria.fr/veridis/

Contacts
Stephan Merz (stephan.merz@loria.fr) and Sophie Tourret (sophie.tourret@loria.fr)

This PhD position is funded by the ANR project BLaSST (Enhancing B Reasoners with SAT and SMT Techniques).

Mission confiée

Context


The B method is a formalism based on set theory that targets the development of software systems used in critical applications, subject to stringent certification requirements. It defines proof obligations that ensure the preservation of invariants or the correctness of refinements between models described at different levels of abstraction, and these proof obligations must be discharged for a model to be accepted as valid.

The application of the B method is supported by Atelier B, maintained by the Clearsy company, a platform that contains several engines for automatic proof. In a recent experiment, among the roughly 77,000 proof obligations of a representative industrial development project, 64% were proved automatically, leaving 28,000 obligations to be proved by human interaction. Also, no significant feedback is provided in case an obligation cannot be proved. Given recent advances in automated theorem proving, we believe that the number of proof obligations that can be discharged automatically can be improved significantly, and that tools can help users by explaining why certain obligations cannot be proved.

The ANR project BLaSST aims at bridging combinatorial and symbolic techniques in automatic theorem proving, in particular for proof obligations arising from models written in the B formalism. 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 instantiation over finite domains. The effectiveness of the techniques developed in the project will be evaluated by applying them to benchmark sets provided by the industrial partner.

BLaSST brings together academic experts in automated reasoning techniques (CRIL, Inria Nancy, and the University of Liège) and the Clearsy company, a leader in the application of formal methods to the design of critical systems, in a 4-year effort that aims to provide a breakthrough in formal verification applied to software design.

Principales activités

Project description

Automated deduction has made significant progress in recent years, including the development of efficient SAT and SMT solvers, and the extension of first-order deduction techniques to fragments of higher-order logic.

The core objective of the thesis is to make these advancements available for system developments in the B method. Concretely, we believe that higher-order logic allows for a much more direct encoding of proof obligations expressed in a language of set theory than existing translations to first-order logic. This should be beneficial for developing specific instantiation techniques that can recognize frequent patterns that arise in B specifications, significantly raising the degree of automation.

A second objective of the thesis is the design of techniques for constructing counter-models in order to provide feedback when a proof fails. Since B models written for industrial developments often contain restrictions to finite-state domains, a stronger integration of SAT solving, beyond just handling the propositional structure of formulas, appears to be beneficial for this objective, as well as for proofs by enumeration.

The thesis will be carried out at the Inria research center in Nancy, France, in close collaboration with the partners of the BLaSST project. The expected starting date is September 1 or October 1, 2022, but a later starting date can be agreed upon.

Compétences

Required qualifications

The candidate must hold (or be about to obtain) a Master degree in computer science. Candidates should have solid knowledge in mathematical logic and preferably in automated reasoning techniques. Experience with formal methods such as B, Alloy, TLA+ or Z would be a plus. The candidate should have mastered a mainstream programming language such as C++, Java or OCaml.

Language

English or French

Avantages

  • Subsidized meals
  • Partial reimbursement of public transport costs
  • Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.)
  • Possibility of teleworking (after 6 months of employment) and flexible organization of working hours
  • Professional equipment available (videoconferencing, loan of computer equipment, etc.)
  • Social, cultural and sports events and activities
  • Access to vocational training
  • Social security coverage

Rémunération

Salary: 1982€ gross/month for 1st and 2nd year. 2085€ gross/month for 3rd year.

Monthly salary after taxes : around 1596,05€ for 1st and 2nd year. 1678,99€ for 3rd year