As the use of concurrent software is increasing, we urgently need techniques to establish the correctness of such applications. Over the last years, significant progress has been made in the area of software verification, making verification techniques usable for realistic applications. However, much of this work concentrates on sequential software, and a next step is necessary to apply these results also on realistic concurrent software. In this paper, we outline a research agenda to realise this goal. We argue that current techniques for verification of concurrent software need to be further developed in multiple directions: extending the class of properties that can be established, improving the level of automation that is available for this kind of verification, and enlarging the class of concurrent programs that can be verified.
|Title of host publication||Principled Software Development|
|Subtitle of host publication||Essays Dedicated to Arnd Poetzsch-Heffter on the Occasion of his 60th Birthday|
|Editors||Peter Müller, Ina Schaefer|
|Place of Publication||Cham|
|Number of pages||18|
|Publication status||Published - 2018|
|Name||Principled Software Development|