More Sophisticated Forms of Model Checking

[hengx...@gmail.com]

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?

Thanks.

Best regards,

Hengfeng Wei

[Karolis Petrauskas]

Maybe one example of that is https://dl.acm.org/doi/10.1145/3360549

Karolis

> --
> 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 tlaplus+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/bef985b2-f0df-4aba-b40f-a2922d828b50n%40googlegroups.com.

[hengx...@gmail.com]

Hi Karolis,

Thanks. That is really amazing and "sophisticated".

Hengfeng

[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. https://link.springer.com/book/10.1007/978-3-319-10575-8

Cheers,
Igor

> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/32994360-0cc7-4194-88ef-376c59826138n%40googlegroups.com.

[hengx...@gmail.com]

Hi Igor,

Thanks for your valuable info.

Best regards,

Hengfeng

[Aman Goel]

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)

Regards

Aman Goel

Ph.D. Student Candidate

Department of Computer Science & Engineering

University of Michigan, Ann Arbor

Web page: https://aman-goel.github.io