< Relaxed Prefix AutoProof Code Repository Rotation >

Ring buffer

Category: Data Structure

Source: VSTTE'12

Description

A bounded queue is implemented using a circular array. The goal is to verify functional correctness of various operations on the queue and client code using the queue.

download source

Code