Rodin

Event-B provides a concise mathematical language for specifying invariants and guards.

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