In this verification example a queue implementation is verified. History-based reasoning is applied to capture the behaviour of the queue, in which the queue is abstracted as a sequence. After using the queue the (process algebraic) history is analysed to see how the shared state has changed.
Atomics, Histories, Sequences
Path to example file
Lines of code
317 lines (comments not included)
Lines of specification
150 lines (47.32% of the total)
Note, verification may take a while and has a time-out of 20 seconds.