[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] More Sophisticated Forms of Model Checking



Hi Igor,

Thanks for your valuable info.

Best regards,
Hengfeng

On Monday, August 9, 2021 at 4:38:56 PM UTC+8 igor....@xxxxxxxxx wrote:
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 <hengx...@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+u...@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/0645914b-c52c-4b9d-8485-c0d2e91698e4n%40googlegroups.com.