Skip to main content
PRL Project

The Logic of Events, a framework to reason about distributed systems

by Mark Bickford, Vincent Rahli, Robert L. Constable

Presented in Philadelphia at the LADA Workshop January 23, 2012

In response to the need of ensuring correctness and security properties of distributed systems and system components in general, programming languages have been developed, featuring rich types such as dependent types or session types, expressive enough to specify such properties. Also, some progress has been done towards automatically proving that programs meet such specifications (often by type checking). Following this line of work, we use constructive logic to synthesize protocols from specifications, and provide tools that facilitate the use of formal methods to prove the correctness of distributed protocols based on asynchronous message passing.

bibTex ref: BCR12

cite link