Relative Safety

Joxan Jaffar, Andrew Santosa and Razvan Voicu


A safety property restricts the set of reachable states. In this paper, we introduce a notion of {\it relative safety} which states that certain program states are reachable provided certain other states are. A key, but not exclusive, application of this method is in representing {\it symmetry} in a program. Here, we show that relative safety generalizes the programs that are presently accommodated by existing methods for symmetry. Finally, we provide a practical algorithm for proving relative safety.