Re: [tlaplus] Modeling Checking Sel4

interactive theorem provers such as Isabelle (underlying the SEL4 project) and model checkers are very different beasts. The former can be used to verify systems of arbitrary complexity, and in particular infinite-state systems, whereas model checking imposes restrictions that ensure that the verification problem is decidable. In particular, the TLA+ model checker TLC is restricted to verify finite-state instances. Most errors can be found over small instances (say, a 3-process version of your algorithm), but it is not always clear if the algorithm is correct in general when the model checker does not find an error for the instances that it can check.

Stephan

On 15 Jun 2019, at 04:52, Imran Meah <imranmeah91@xxxxxxxxx> wrote:

I studied formal verification of SEL4 using theorem proving It is quite extensive and requires years of manual effort I was wondering if model checking tools like TLA+ can be used for that.

Also, I observed that in addition to checking for safety and liveness properties, they also prove functional correctness, is something like that possible with model checking.

--
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/6e00f305-5154-4287-97ab-1ca7ec6d5005%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.