Property Directed Self Composition

Ron Shemer, Arie Gurfinkel, Sharon Shoham +1

We address the problem of verifying k-safety properties: properties that refer to k-interacting executions of a program. A prominent way to verify k-safety properties is by self co…