Model Checking TLA+ Specifications
- Yuan Yu ,
- Panagiotis Manolios ,
- Leslie Lamport
In Correct Hardware Design and Verification Methods (CHARME '99), Laurence Pierre and Thomas Kropf editors. Lecture Notes in Computer Science, Springer-Verlag. |
Despite my warning him that it would be impossible, Yuan Yu wrote a model checker for TLA+ specifications. He succeeded beyond my most optimistic hopes. This paper is a preliminary report on the model checker. I was an author, at Yu’s insistence, because I gave him some advice on the design of the model checker (more useful advice than just don’t do it). Manolios worked at SRC as a summer intern and contributed the state-compression algorithm that is described in the paper, but which ultimately was not used in the model checker.