PhD Positions Available in Formal Methods for Reversible Concurrent Calculi, Georgia (USA)

The Concurrency In Reversible Computations project at Augusta University (Georgia, USA) is actively seeking a PhD student to fund starting as Fall 2024 or Spring 2025. The successful applicant will be advised by Clément Aubert, and benefit from an international network of collaborators, as well as from a local, lively, group of PhD students (including but not limited to students working on related formal methods). In addition, they will have the opportunity to help mentoring undergraduate research assistants if they wish to do so.

The main goals of this project are to improve existing process calculi formalizing reversible computations. In the past, reversible calculi have shed a new light on the correctness and adequation of CCS, π-calculus and other formalisms for concurrent computation, but they still miss crucial features. Contextual equivalences, observable behaviors, set of operators and infinite behavior, to name a few, are still in the flux and in need of formal definitions that adequately models interesting systems. The original project encompasses many different dimensions, and will be tailored based on mutual interests, capacities, and recent progresses.