Cav2024

This directory contains the illustrative examples from the paper, in Ivy

• examp1.ivy: Example of Fig. 1 using relational ranking
• examp1_l2s.ivy: same, using DL2s
• examp1_numeric.ivy: same, using numeric ranking
• examp2.ivy: Section 3.2, chaining liveness lemmas
• examp3.ivy: Section 3.3, cascaded queues
• examp4.ivy: Section 3.3, cascaded queues with blocking
• examp5.ivy: Section 3.4, cascaded queues with bypassing

Run the examples with this command:

$ ivy_check <file>.ivy