Safety and liveness properties - WikipediaProperties of an execution of a computer program—particularly for concurrent and distributed systems—have long been formulated by giving safety properties ("bad things don't happen") and liveness properties ("good things do happen").[1] A program is totally correct with respect to a precondition and postcondition if any execution started in a state satisfying terminates in a state satisfying . Tot
