Output details

Correct-by-Construction Concurrency : Using Dependent Types to Verify Implementations of Effectful Resource Usage Protocols

<08>This paper presented a novel approach to verifying absence of deadlock and race conditions in concurrent programs. We show that, by capturing the required operations and their pre- and post-conditions in a Domain Specific Language embedded in a dependently-typed programming language, a concurrent program can be proven to have the desired properties by construction.

This was one of the first papers to give a practical example of systems verification with dependent types, with a working implementation. This work has led to several further papers on resource verification, and these ideas have driven further development of the Idris programming language.