# 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.