More Sophisticated Forms of Model Checking

Skip to first unread message

Aug 7, 2021, 3:32:01 AMAug 7
to tlaplus
I am reading the paper "Real Time is Really Simple" by Leslie Lamport.

It reads at the beginning of Section 6.1:
"Model checking a specification consists of mechanically verifying that all
possible executions satisfy the desired correctness properties. Specifications
typically contain unspecified parameters, such as the number of processes
or the size of a buffer. Ordinary model checking is performed for specific
instances of the specification obtained by substituting actual values for the
parameters. The likelihood that model checking has missed an error in the
specification depends on the variety of different instances that have been
checked. There are more sophisticated forms of model checking that employ
abstraction techniques, sometimes with simple mechanical theorem check-
ing, to verify the specification for all values of the parameters."

Do you know any resources for such "more sophisticated forms of model checking", such as papers and examples?


Best regards,
Hengfeng Wei

Karolis Petrauskas

Aug 7, 2021, 4:12:33 AMAug 7
Maybe one example of that is

> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to
> To view this discussion on the web visit

Aug 7, 2021, 8:32:48 AMAug 7
to tlaplus
Hi Karolis,

Thanks. That is really amazing and "sophisticated".


Igor Konnov

Aug 9, 2021, 4:38:56 AMAug 9
to, Igor Konnov
Hi Hengfeng,

Thanks that you like our paper :-)

Concerning model checking, there are really plenty of papers, techniques, and tools, so it would be easier to start with a textbook, e.g., [1]. You can always check proceedings of the conferences such as CAV, POPL, VMCAI, FMCAD, SPIN, NFM. I think most of them had open access proceedings in the last years. However, conference proceedings contain research papers that usually do not provide a beginner with detailed context.

The main issue with many of the advanced model checking techniques is that they limit the computational model to make model checking fast. If you have a TLA+ spec, it may take you considerable time to make it fit into one of those fragments. Transferring advanced techniques to TLA+ is still a research challenge.

[1] Clarke et al. Handbook of Model Checking, 2018.

> To view this discussion on the web visit

Aug 9, 2021, 12:44:47 PMAug 9
to tlaplus
Hi Igor,

Thanks for your valuable info.

Best regards,

Aman Goel

Aug 9, 2021, 1:22:10 PMAug 9
to tlaplus
Hi Hengfeng,

Building on previous efforts, I recently developed one such model checking technique that you may find interesting [1], [2].

[1] Aman Goel, and Karem Sakallah. "On Symmetry and Quantification: A New Approach to Verify Distributed Protocols." In NFM, 2021. (arXiv)
[2] IC3PO: IC3 for Proving Protocol Properties (GitHub)

Aman Goel
Ph.D. Student Candidate
Department of Computer Science & Engineering
University of Michigan, Ann Arbor

Reply all
Reply to author
0 new messages