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 verification with the new algorithm is often significantly faster than with standard model checking.

• Type: Journal
• Year: 2010
• Where: CAV
• Authors: Ariel Cohen 0002, Kedar S. Namjoshi, Yaniv Sa'ar
• Keywords: CAV 2010, Fairness Assumptions, Global Fairness Assumptions, Hardware, Local Reasoning