Model Checking Event-B by Encoding into Alloy

Paulo J. Matos, Joao Marques-Silva

As systems become ever more complex, verification becomes more main stream. Event-B and Alloy are two formal specification languages based on fairly different methodologies. While…