Rodin

Event-B provides a concise mathematical language for specifying invariants and guards. While both Event-B and Rodin matured, certain …

In a previous work, we applied constraint solving techniques to problems like invariant preservation and deadlock freedom checking. The …