Reasoning about nondeterministic programs requires a specification of how their nondeterministic choices are allowed to be resolved. When reasoning about safety properties, it is sound to overapproximate the permitted behaviors. Once its safety is established, a program remains safe for every valid implementation of its nondeterministic choices. Overapproximate specifications are less useful when establishing that a nondeterministic program exhibits some desirable behavior, however, as resolving nondeterminism to specific choices is not guaranteed to preserve the execution that resulted in the desirable final state. This paper proposes a flexible way to underapproximate the behaviors of nondeterministic choices so that clients can soundly reason about the existence of desirable behaviors, while at the same time permitting some freedom in how those choices are implemented. We present a pair of program logics, called HLE and RHLE, that use these specifications to reason about existential program behaviors in the single program and relational settings, respectively. We have implemented a verifier based on these program logics that is capable of automatically verifying a wide range of relational properties, including refinement and noninterference. We have evaluated our approach by using this tool to verify a diverse set of programs and properties drawn from the literature.
分享
引用
