Various subjects are possible, centered on formal methods anywhere in computing science. For inspiration you could join our weekly reading group.
1. The challenge is to construct a refinement proof of Bloom's algorithm (IEEE Trans. Comp. 37, 1988) and to verify it mechanically with the proof assistant PVS, as used in the course on Automated Reasoning. The main ingredients of the proof seem to be available in my papers in Acta Inf. 38 (2002) and SCP 71 (2008), but an integrated proof is lacking yet.
2. Investigate the mutual exclusion algorithm BW of Block and Woo (Information Processing Letters 35 (1990) 219-222), and compare it with the one described here. You could make a mechanical proof of BW, or perhaps a refutation based on a scenario.
3. Mechanical proofs of graph algorithms with PVS. This research builds on the master course on Automated Reasoning, but of course also on the bachelor courses Program Correctness and Algorithms and Data Structures. There are several candidate algorithms to try and treat. One of them is the so-called "stressing algorithm" to determine the existence of negative weight cycles in weighted directed graphs. This may give an interesting case study to include in a publication about the treatment of sequential algorithms with PVS and the theory of programs.
Eén mogelijk afstudeeronderwerp is het gebruik van een stellingbewijzer bij het ontwerp en de verificatie van gedistribueerde algoritmen en systemen. In gedistribueerde algoritmen (zoals behandeld in het vak Concurrency) kunnen verschillende processen op moeilijk te voorziene wijze interfereren. Als je weet welke eigenschappen je invariant wilt houden, is dat met een stellingbewijzer gemakkelijker na te gaan dan uit het hoofd of met de hand. Het grootste voordeel blijkt echter pas als je het algoritme wil veranderen: je kunt dan namelijk het oude bewijs opnieuw ``afspelen''. De bewijzer stokt dan op die punten waar het oude bewijs moet worden aangepast. Doordat de bewijzer de administratie over de bewezen invarianten bijhoudt, kan een ingewikkelder ontwerp in lagen worden opgebouwd zonder dat de lagen eerst afzonderlijk hoeven te worden uitgetest.
Een voorbeeldproject is ``Logically Synchronous Multicasts'' (voortzetting van het afstudeerproject van David Hoogvorst). Elk ander interessant gedistribueerd algoritme kan echter ook.
There are many other subjects, e.g., in the sphere of program correctness. In some cases, we may want to rely on handwritten proofs, rather than mechanically verified ones, or to use model checkers.
Last modified: Mon Dec 8 09:56:22 CET 2008Back to my educational page or to my home page.
Wim H. Hesselink