nbacg_guer01 Specification's authors: Thanh Hai Tran, Igor Konnov, Josef Widder Original paper: Extended modules: Nat, FinSet Computation models: clean crashes Some properties checked with TLC: agreement, validity, integrity, termination