  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 composition. In this approach, the problem of
checking k-safety over the original program is reduced to checking an
"ordinary" safety property over a program that executes k copies of the
original program in some order. The way in which the copies are composed
determines how complicated it is to verify the composed program. We view this
composition as provided by a semantic self composition function that maps each
state of the composed program to the copies that make a move. Since the
"quality" of a self composition function is measured by the ability to verify
the safety of the composed program, we formulate the problem of inferring a
self composition function together with the inductive invariant needed to
verify safety of the composed program, where both are restricted to a given
language. We develop a property-directed inference algorithm that, given a set
of predicates, infers composition-invariant pairs expressed by Boolean
combinations of the given predicates, or determines that no such pair exists.
We implemented our algorithm and demonstrate that it is able to find self
compositions that are beyond reach of existing tools.
