PhD proposal: Leveraging Automatic Deduction for Verification

The full description of the PhD proposal is available here.

Topics

Computer Science, Logic, Automatic and Interactive Theorem Proving, Satisfiability Modulo Theo- ries, Higher-Order Logic, Induction, Verification

Institution

Inria, Loria, Université de Lorraine (in cooperation with VU Amsterdam)

Location

Nancy, France (in cooperation with Amsterdam, The Netherlands)

Research Group

VeriDis

Supervision

Stephan Merz, Pascal Fontaine, Jasmin Blanchette

Background

This PhD subject is proposed in the context of Jasmin Blanchette’s ERC Starting Grant Matryoshka, an ambitious five-year project that aims at making automatic provers more useful for interactive verification by reducing the gap between the automatic and interactive worlds.

The TLA+ Proof System (TLAPS) is a platform for mechanically checking proofs for system specifications written in the TLA+ language, based on Zermelo-Fraenkel set theory and the Temporal Logic of Actions (TLA), a variant of linear-time temporal logic. TLA+ is a general- purpose formal specification language that is particularly well-known for describing concurrent and distributed algorithms and systems. It has seen significant use in academia and industry, including Amazon, Intel, Microsoft and many others.

In previous work, we have already defined an overall strategy for encoding TLA+’s set theory into first-order logic. Our encoding has been implemented within TLAPS for translating TLA+ proof obligations to the input languages of Satisfiability Modulo Theories (SMT) solvers and first-order provers, and we have demonstrated a reduction of proof effort, measured as the number of user interactions, by one or two orders of magnitude for obligations that mix elementary set theory, basic integer arithmetic, and first-order logic.

The overall ambition of the present thesis is to build upon this success and significantly improve the scope of automation within TLAPS, by building upon, and contributing to, the advances in Satisfiability Modulo Theories solvers within the scope of the Matryoshka project. This includes support for important data structures, such as sequences, that are outside the scope of the current SMT encoding. It also aims at leveraging the work within Matryoshka on lifting the reasoning capabilities of SMT solvers towards higher-order logic, including support for inductive reasoning and complex set-theoretic expressions such as set comprehension.

Objectives

Building on our previous work, this thesis will design new techniques of automatic proof and make them available within TLAPS in order to further increase automation for deductive verification. We envisage the following possible directions:

  • design decision procedures that support important data structures of TLA+ such as finite sequences. Their theoretical properties (soundness, completeness, and complexity) will be analyzed, and they will be implemented as a prototype;
  • exploit new capabilities of SMT solvers for higher-order reasoning, in particular for supporting proofs by inductive reasoning and for set comprehensions;
  • use proofs and models to improve confidence and guidance in verification platforms;
  • develop effective and complete techniques for iterative refinement of the translation into the solver language, in particular concerning the expansion of operator definitions;
  • analyze the specification and proof obligations in order to provide hints for proof search in SMT, notably for instantiation: we aim at providing syntactic criteria and characterizing decidable fragments.

The results of the thesis will be of primary interest to users of TLA+, but they can also be relevant for related set-based specification formalisms such as Event-B, and the associated verification platforms, such as Rodin. The subject can and will be adjusted according to the interests of the PhD candidate, in particular for choosing which of the above directions will be pursued first.

Requirements

We are looking for excellent candidates with a strong interest for logic, decision procedures, proofs and verification. Some acquaintance with either automated, interactive theorem proving, or deductive verification platforms is a plus. Knowledge of French is not required. The student will work in an international environment, in collaboration with several PhD students and experienced scientists.

How To Apply

Send the following documents to stephan.merz@loria.fr in a single ZIP file:

  • your up-to-date CV,
  • an accompanying letter explaining your motivation and background for carrying out this project,
  • your degree certificates and transcripts for your Bachelor and Master degrees (or the last five years if not applicable),
  • your Master thesis (or equivalent) if it is already completed or a description of the work in progress otherwise,
  • your publications if any (it is not expected that you have already published).

In addition, at least one letter of reference written by the person who supervises your Master thesis (or research project or internship) must be provided. At most two other recommendation letters may be sent. These letters should be sent directly to stephan.merz@loria.fr.

Benefits

  • Monthly net salary of approximately 1600 euros, medical insurance included.
  • Possibility of free French courses.
  • Help with finding accommodation and administrative procedures (such as obtaining a visa).
  • Subsidized lunch at the Inria restaurant.

No offers are available for now.

Now

Logo du CNRS
Logo Inria
Logo Université de Lorraine