ERC Consolidator Grant · 2016
Type and Proof Structures for Concurrent Software Verification
Verification of concurrent software is a notoriously difficult subject, whose complexities stem from the inability of the existing verification methods to modularize, and thus divide-and-conquer, the verification problem. Dependent types are a formal method well-known for its ability to modularize and scale complex mathematical proofs. But, when it comes to programming, dependent types are considered limited to the purely functional and terminating programming model. The grand challenge of this project is to remove the limitation and scale dependent types to support implementation of stateful concurrent programs, and their correctness proofs, simultaneously. By applying the modularizing…
From the public funding record at EU CORDIS. Describes the funded project, not the reviews below.