Concurrent GCD
Category: Algorithm
Source: ETAPS'15
Description
Find the GCD of two natural numbers using two execution threads, each of which only updates one variable; since AutoProof doesn't support concurrency, we model this aspect with nondeterminism and prove that the algorithm terminates assuming a fair scheduler.