|Persons involved in the project|
|Activities and Results|
In safety critical systems, concurrent programs become more widespread, even though their correctness is particularly difficult to ascertain, because system failures due to timing problems are hard to detect with traditional quality insurance methods like tests. Untimely or badly synchronized access to resources may lead to data corruption, with catastrophic consequences.
This project aims at providing a technical contribution, by investigating analysis and verification techniques for concurrent programs, and a methodological contribution, by relating program analyses and proof methods in a demonstrably sound way. This foundational work will be accompanied by the implementation of an IDE and will carry out experimental evaluations and case studies demonstrating that the approach is usable in practice.
|Last modified: Wed Dec 31 22:13:01 CET 2014|