History-based reasoning: verifying a queue

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.

General information

ID83
Articlenone
Back-endSilicon
LanguageJava
FeaturesAtomics, Histories, Sequences
Sources
Path to example filelayers/LFQHist.java
Date2017-06-20

Statistical information

Lines of code317 lines (comments not included)
Lines of specification150 lines (47.32% of the total)
Computation time52104 milliseconds

Example code

Note, verification may take a while and has a time-out of 20 seconds.