Re: [tlaplus] More Sophisticated Forms of Model Checking

[Karolis Petrauskas <k.petrauskas@xxxxxxxxx>]

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
<hengxin0912@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+unsubscribe@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/CAFteovJKOBi%3DwGQoGPThRdXjEzhSE%2B-1uTW1Mt6G91wf4j2Qiw%40mail.gmail.com.