The Mapper
We used the Tomte tool [AHKOV12] to automatically construct a mapper for the Login system. Using counterexample-guided abstraction refinement, Tomte is able to automatically infer guard statements containing equality of data parameters and constants.
