Relative Safety
Joxan Jaffar, Andrew Santosa and Razvan Voicu
Abstract
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.