Internship 2024–2025: Verification for the Varda distributed programming language
Keywords
Distributed systems; distributed programming; programming languages and verification; composition; system architecture
Background
Distributed systems are increasingly widespread and critical. A typical distributed system composes independent modules, which execute concurrently and communicate with one another through message-based APIs. This modular approach promotes software reuse, flexibility, and independent execution. However, understanding the behavior of a composition is hard, because of concurrency, failures, and weak guarantees (such as type checking).
The Varda distributed programming language aims to leverage the power of distributed computing and the strengths of modularity, reconciling strong abstractions and performance. Varda helps the developer reason about components both individually and in composition, while preserving performance and programmer control.
A Varda program specifies a system as an architecture of independently-developed components. Each component has a well-specified protocol interface and high-level safety constraints, while Varda orchestration specifies how components are created and destroyed, where they are located, how they interact, and what invariants they must maintain. A Varda system can be re-architected flexibly thanks to transparent interception.
The Varda compiler verifies component interactions, and generates glue code between modules and between modules and with the environment. The compiler is highly modular, provides extension hooks, and can support multiple code-generation backends.
Internship perspectives
The current Varda compiler already performs a repertoire of static verification, including both message data types and protocol correctness (session types). The compiler inserts dynamic assertions to check preconditions and postconditions at runtime. The compiler is equipped with hooks, intended to be used to extend the compiler.
The goal of the internship is to improve the verification capabilities of the Varda compiler, in order to verify statically global properties, such as invariants. The intern shall work on two fronts: improving its type system, and exporting a Varda architecture as a formal model to an external checker (e.g., TLC, Coq or P), in order to statically verify specific properties.
Requirements and application
The internship will be advised by Alessio Pagliari of Sorbonne-Université, by Marc Shapiro of Sorbonne-Université and Inria, and by Ahmed Bouajjani, of IRIF. It will take place in Paris, France. Speaking French is not required.
The candidate should ideally be interested in distributed systems and be familiar with compilation and formal approaches (e.g., model-checking).
He/she should also have a basic experience in software programming in OCaml, and collaborative development tools such as git.
Please contact the advisors Marc Shapiro <marc.shapiro@acm.org> and Alessio Pagliari <alessio.pagliari@lip6.fr>, with the following information:
- A resume or Curriculum Vitæ.
- A motivation letter.
- A list of courses and grades of the last two years of study (an informal transcript is OK).
