We are designing a formal synthesis framework, embedded in Coq, for building proven-to-be-correct message-passing systems. The framework provides a way of specifying protocols at a high-level. A synthesizer tries to build an executable implementation that is formally proven to follow the specification. Synthesized implementations may involve a lot of interleavings, where the safety of such interleavings is automatically guaranteed by the synthesis process. As a case study, we are currently trying to synthesize various cache-coherence protocols.
If you would like to contact us about our work, please scroll down to the people section and click on one of the group leads' people pages, where you can reach out to them directly.