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

  • Backend: Silicon
  • Language: Java
  • Features: Sequences, Atomics, Histories
  • Path to Example File: layers/LFQHist.java
  • Should Verify: Yes
  • Date: 2017-06-20
  • Lines of Code: 317 (comments not included)
  • Lines of Specification: 150 (47.3% of total)
  • Computation Time: 52.1 seconds