Bounded Model Checking for Hyperproperties
share
This paper introduces the first bounded model checking (BMC) algorithm for hyperproperties expressed in HyperLTL. Just as the classic BMC technique for LTL primarily aiming at finding bugs, our approach also targets identifying counterexamples. LTL describes the property of individual traces and BMC for LTL is reduced to SAT solving. HyperLTL allows explicit and simultaneous quantification over traces and describes the property of multiple traces and, hence, our BMC approach naturally reduces to QBF solving. We report on successful and efficient model checking of a rich set of experiments on a variety of case studies, including security/privacy, concurrent data structures, and path planning in robotics applications.
READ FULL TEXT