spanning Specification's authors: Thanh Hai Tran, Igor Konnov, Josef Widder Original paper: Extended modules: Int Computation models: no faults Some properties checked with TLC: OneParent, termination