CTIT University of Twente
Research Business & Innovation About CTIT Research Calls Looking for a job? Intranet

VerDi: Verification of Distributed Data Structures

Project Number:

Project Manager: Prof. dr. Marieke Huisman

Faculty of Electrical Engineering, Mathematics and Computer Science

Tel.: +31-53-4894662

Email: M.Huisman@utwente.nl

Project website: VerDi

Summary

The VerDi project studies the Verification of Distributed Data Structures. Its aim is to develop automated program-logic based techniques for (message-based) dis- tributed 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 communic-ation 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 experience and 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. Within the VerDi project, we aim to show that separation logic is also suitable to verify distributed programs running on multiple computers. In particular, it will be used 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. All techniques will be validated on realistic and relevant examples.

Project duration: 2014-2018

Number of person/months: 106 person months

Project Coordinator: UT

Participants: UT, INRIA Grenoble

Project budget CTIT: 165 k-€ funding

Number of person/years CTIT: 30,2 person months

Involved groups: Formal Methods and Tools

CTIT Research Centre: Centre for Safety and Security in Smart Societies (C.S4)