Verifying Safety Properties Using Non-Deterministic Infinite-State Automata.

摘要

A new class of infinite-state automata, called safety automata, is introduced. Any safety property can be specified by using such an automation. Sound and complete proof obligations for establishing that an implementation satisfies the property specified by a safety automaton are given. Keywords: Computer program verification, Concurrent programming, Temporal logic. (KR)