University of Twente Student Theses

Login
As of Friday, 8 August 2025, the current Student Theses repository is no longer available for thesis uploads. A new Student Theses repository will be available starting Friday, 15 August 2025.

Formal Automated Verification of a Work-Stealing Deque

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

[img] PDF
271kB
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)
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:https://purl.utwente.nl/essays/80687
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page