BLaSST is a project funded by ANR, the French research agency. It involves the VeriDis team of Inria in Nancy, the CRIL laboratory of University of Artois in Lens, the CLEARSY company, and the Montefiore Institute of University of Liège in Belgium. BLaSST was selected for funding as project ANR-21-CE25-0010.

The project started in March 2022 and runs until February 2026.

Two PhD positions are available within BLaSST.

SAT-based approaches for formal verification with the B method

This position 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 position is located in Lens (France), at the CRIL research laboratory. The PhD candidate will have 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 a mainstream programming language such as C, C++ or Java.

Contacts:

Apply here

Automated Reasoning for Set Theory

The core objective of the thesis is to make recent advancements in automated deduction available for system developments in the B method. It will focus on the following objectives:

  • Design encodings of B proof obligations in higher-order logic.
  • Develop specific instantiation techniques for patterns that arise frequently in B specifications, in order to significantly raise the degree of automation with which proof obligations can be discharged.
  • Design techniques for constructing counter-models in order to provide feedback when a proof fails.

The position is located in Nancy (France) at the VeriDis team of Inria Nancy. The PhD candidate will have a master degree (or equivalent) in computer science and 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 master a mainstream programming language such as C++, Java or OCaml.

Contacts:

Apply here