[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] More Sophisticated Forms of Model Checking
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
> 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
> 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.