Re: [tlaplus] More Sophisticated Forms of Model Checking

[Igor Konnov <igor.konnov@xxxxxxxxx>]

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

> On 07.08.2021, at 14:32, hengx...@xxxxxxxxx <hengxin0912@xxxxxxxxx> wrote:
> 
> Hi Karolis,
> 
> Thanks. That is really amazing and "sophisticated".
> 
> Hengfeng
> On Saturday, August 7, 2021 at 4:12:33 PM UTC+8 k.petr...@xxxxxxxxx wrote:
> Maybe one example of that is https://dl.acm.org/doi/10.1145/3360549 
> 
> Karolis 
> 
> On Sat, Aug 7, 2021 at 10:32 AM hengx...@xxxxxxxxx 
> <hengx...@xxxxxxxxx> wrote: 
> > 
> > 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 
> > 
> > -- 
> > 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...@xxxxxxxxxxxxxxxx. 
> > To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/bef985b2-f0df-4aba-b40f-a2922d828b50n%40googlegroups.com. 
> 
> -- 
> 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+unsubscribe@xxxxxxxxxxxxxxxx.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/32994360-0cc7-4194-88ef-376c59826138n%40googlegroups.com.

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/071CE7B0-4508-4313-BC64-65DCAA21E6F6%40gmail.com.