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
About
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.