Parallel GCD

In this example a concurrent GCD algorithm is proven correct, meaning that after the algorithm terminates it has calculated the GCD of the two input values. The verification is done by using model-based abstraction. A process algebraic model of the GCD algorithm is defined and we prove that the program adheres to this abstraction. By analysing the process algebra term we finally verify that the program calculates the correct GCD.

General information

ID61
Articlenone
Back-endSilicon
LanguagePVL
FeaturesFutures, Statically-scoped locking, Statically-scoped parallelism
SourcesVerifyThis competition 2015
Path to example filefutures/ParallelGCD.pvl
Date2017-06-16

Statistical information

Lines of code80 lines (comments not included)
Lines of specification37 lines (46.25% of the total)
Computation time24919 milliseconds

Example code

Note, verification may take a while and has a time-out of 20 seconds.