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

Presented in Philadelphia at the LADA Workshop January 23, 2012

position paper: [PDF]

slides: [PDF]

by Mark Bickford, Vincent Rahli, and Robert L. Constable


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.

Back to publication list