Anzeige
Erschienen in:
2010 | OriginalPaper | Buchkapitel
A Dash of Fairness for Compositional Reasoning
verfasst von : Ariel Cohen, Kedar S. Namjoshi, Yaniv Sa’ar
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Proofs of progress properties often require fairness assumptions. Directly incorporating global fairness assumptions in a compositional method is difficult, given the local flavor of such reasoning. We present a fully automated local reasoning algorithm which handles fairness assumptions through a process of iterative refinement. Refinement strengthens local proofs by the addition of auxiliary shared variables which expose internal process state; it is needed as local reasoning is inherently incomplete. Experiments demonstrate that the new algorithm shows significant improvement over standard model checking.