University of Twente Student Theses


Formal Automated Verification of a Work-Stealing Deque

Kampen, C.M. van (2020) Formal Automated Verification of a Work-Stealing Deque.

[img] PDF
Abstract:Multi-core systems brought the possibility for concurrent programs. In task-based parallelism, work-stealing has been an important development. Many designs of a work-stealing framework make use of deques, but they do not properly prove the correctness of the deque. Therefore, the deque from the Lace framework has been implemented and verified for functional correctness using the VerCors verification tool. Under our assumptions, the verification in VerCors passes and shows that all tasks are executed and return the correct result. The verification has been partially validated, but more testing and validation is required before a statement can be made about the validity of the proof.
Item Type:Essay (Bachelor)
Unknown organization, Enschede, Netherlands
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science BSc (56964)
Keywords:Concurrency, Task-based parallelism, Deque, Work-stealing, Deductive verification, VerCors
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page