1. 10
  1.  

  2. 1

    I’ve used (something like) this with Tamarin, and it is immensely useful when working with provers that employ a high degree of automation.

    1. 1

      I’ve used formal method tools at a few jobs, and I think something like this is incredibly important. Trying to introduce these concepts with “just traces” is not enough for a lot of people. They need to interact and see the effects of their choices on the system. That interaction, gives meaning and trust to them for these processes and tools.

      One of the reasons my go-to tool for understanding and specifying these days is mcrl2 simply because it makes interaction with the spec so easy with it’s simulation tools. But I often find the difficulty of getting to traces troubling.

      1. 1

        One of the reasons my go-to tool for understanding and specifying these days is mcrl2 simply because it makes interaction with the spec so easy with it’s simulation tools. But I often find the difficulty of getting to traces troubling.

        I’ve tried to learn mcrl2 a few times and keep bouncing off. Someone needs to write a good showboating example for it!