Computing and Proving Well-founded Orderings through Finite Abstractions

Rob Sumners

A common technique for checking properties of complex state machines is to build a finite abstraction then check the property on the abstract system -- where a passing check on the…