Some examples using the Invariant Checker

Some examples using the Invariant Checker:

These are some examples treated using the Invariant Checker. The examples are given in the syntax used in the tool.
  • A simple example
  • Peterson mutual exclusion algorithm
  • Bakery mutual exclusion algorithm
  • An alternating bit protocol
    • Back to the Invariant Checker home page