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.