[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] More Sophisticated Forms of Model Checking
Building on previous efforts, I recently developed one such model checking technique that you may find interesting , .
 Aman Goel, and Karem Sakallah. "On Symmetry and Quantification: A New Approach to Verify Distributed Protocols." In NFM
, 2021. (arXiv
 IC3PO: IC3 for Proving Protocol Properties (GitHub
Ph.D. Student Candidate
Department of Computer Science & Engineering
University of Michigan, Ann Arbor
Web page: https://aman-goel.github.io
On Monday, August 9, 2021 at 12:44:47 PM UTC-4 hengx...@xxxxxxxxx wrote:
Thanks for your valuable info.
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., . 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.
 Clarke et al. Handbook of Model Checking, 2018. https://link.springer.com/book/10.1007/978-3-319-10575-8
> On 07.08.2021, at 14:32, hengx...@xxxxxxxxx <hengx...@xxxxxxxxx> wrote:
> Hi Karolis,
> Thanks. That is really amazing and "sophisticated".
> 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
> 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/1a78a13e-3949-4801-a3d7-7242f8c72259n%40googlegroups.com.