Abstract Patterns of Compositional Reasoning

Patterns of Compositional Reasoning Nina Amla1 , E. Allen Emerson2 , Kedar Namjoshi3 , and Richard Trefler4 1 Cadence Design Systems 2 Univ. of Texas at Austin 3 Bell Labs, Lucent Technologies 4 Univ. of Waterloo Abstract. Compositional Reasoning – reducing reasoning about a concurrent system to reasoning about its individual components – is an essential tool for managing proof complexity and state explosion in model checking. Typically, such reasoning is carried out in an assume-guarantee manner: each component guarantees its behavior based on assumptions about the behavior of other components. Restrictions imposed on such methods to avoid unsoundness usually also result in incompleteness – i.e., one is unable to prove certain properties. In this paper, we conn abstract framework for reasoning about process composition, formulate an assume-guarantee method, and show that it is sound and semantically complete. We then show how to instantiate the framework for several common noti...

• Type: Conference
• Year: 2003
• Where: CONCUR
• Authors: Nina Amla, E. Allen Emerson, Kedar S. Namjoshi, Richard J. Trefler
• Keywords: Compositional Reasoning, Compositional Reasoning Nina, CONCUR 2003, Reasoning