In the Formal Methods and Tools (FMT) research group, formal techniques and tools are developed and used as a means to support the development of software. This includes the development of formal theories of concurrency, design methodologies for distributed systems, and correctness assessment using verification or validation techniques. The group is also concerned with the development of traditional tools such as compilers and interpreters. In both research and courses much attention is paid to the applicability of formal methods.

The FMT group is part of the Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS) at the University of Twente.

Aim of the VerDi project is to develop automated program-logic based techniques for (message-based) distributed software.

Developing techniques to ensure the correctness of such programs is of utmost importance, because they are widely used for many different applications, including safety-critical ones. Typical examples are air traffic control systems and communication networks for emergency services. At the same time, this is also a considerable challenge, because in distributed programs the exchanged messages can arrive in arbitrary order or even get lost, so that a single program can show many different behaviours.

Current research on the verification of distributed programs focuses mostly on message exchange between the different sites, modelled at an abstract level, without considering implementation details. The VerDi project will bridge the gap between the abstract and the implementation level, and enable reasoning about the actual distributed software.

The VerDi project builds on ongoing work in the VerCors project, where a specific program logic, called separation logic, is used to verify concurrent software i.e., programs that run on a single computer.

The PhD candidate we are looking for is expected to develop a variant of separation logic that is also suitable to verify distributed programs running on multiple computers. In particular, the logic should be usable to explore distributed implementations of data structures. To specify the behaviour of data structures, it is essential that the logic is really on the level of the program code. We expect that recent techniques on using history-based reasoning to capture functional properties of concurrent programs also can be applied in a distributed setting. All techniques will should be validated on realistic and relevant examples.