Paper Info
Title
On the Competeness of Compositional Reasoning
Abstract
Several proof rules based on the assume-guarantee paradigm have been proposed for compositional reasoning about concurrent systems. Some of the rules are syntactically circular in nature, in that assumptions and guarantees appear to be circularly dependent. While these rules are sound, we show that several such rules are incomplete, i.e., there are true properties of a composition that cannot be deduced using these rules. We present a new sound and complete circular rule. We also show that circular and non-circular rules are closely related. For the circular rules defined here, proofs with circular rules can be efficiently transformed to proofs with non-circular rules and vice versa.
Year
DOI
Venue
2000
10.1007/10722167_14
CAV
Keywords
Field
DocType
compositional reasoning,rule based
Computer science,Concurrency,Algorithm,Theoretical computer science,Mathematical proof,Compositional reasoning,Versa,Formal verification
Conference
ISBN
Citations 
PageRank 
3-540-67770-4
29
1.19
References 
Authors
20
2
Name
Order
Citations
PageRank
Kedar S. Namjoshi194850.41
Richard J. Trefler222214.59