< Composite AutoProof Code Repository Dancing Links >

Concurrent GCD

Category: Algorithm

Source: ETAPS'15


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.

download source