Verification of boost's concurrent data structures
The aim of this task is to verify two parallel structures of Boost - lock- free queue and lock-free stack. The task could be divided into few subtasks:
- Compile DIVINE
- Read the paper (http://www.cs.rochester.edu/~scott/papers/1996_PODC_queues.pdf)
- Compile Boost library with dummy main
- Specify and implement test-cases
- Verify test-cases with DIVINE
- Analyse results
- Sumarize results and make a presentation.