A Dash of Fairness for Compositional Reasoning

Abstract. Proofs of progress properties often require fairness assumptions. Incorporating global fairness assumptions in a compositional method is a challenge, however, given the local flavor of such reasoning. We present a fully automated local reasoning algorithm which handles fairness assumptions. As local reasoning is inherently incomplete, the algorithm incorporates a refinement step, which strengthens local proofs by adding auxiliary shared variables. Experiments show that the compositional algorithm shows significant improvement over standard model checking.