Proof rules for automated compositional verification through learning Export

@inproceedings{citeulike:3452604, abstract = {Compositional proof systems not only enable the stepwise development of concurrent processes but also provide a basis to alleviate the state explosion problem associated with model checking. An assume-guarantee style of specification and reasoning has long been advocated to achieve compositionality. However, this style of reasoning is often nontrivial, typically requiring human input to determine appropriate assumptions. In this paper, we present novel assumeguarantee rules in the setting of finite labelled transition systems with blocking communication. We show how these rules can be applied in an iterative and fully automated fashion within a framework based on learning.}, author = {Barringer, Howard}, booktitle = {In Proc. SAVCBS Workshop}, citeulike-article-id = {3452604}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.3.8668}, keywords = {agdaspin, assume-gurantee-reasoning, copy, model-checking}, pages = {14--21}, posted-at = {2008-10-27 08:27:47}, priority = {2}, title = {Proof rules for automated compositional verification through learning}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.3.8668}, year = {2003} }

TY - CONF ID - citeulike:3452604 L3 - citeulike-article-id:3452604 N2 - Compositional proof systems not only enable the stepwise development of concurrent processes but also provide a basis to alleviate the state explosion problem associated with model checking. An assume-guarantee style of specification and reasoning has long been advocated to achieve compositionality. However, this style of reasoning is often nontrivial, typically requiring human input to determine appropriate assumptions. In this paper, we present novel assumeguarantee rules in the setting of finite labelled transition systems with blocking communication. We show how these rules can be applied in an iterative and fully automated fashion within a framework based on learning. EP - 21 TI - Proof rules for automated compositional verification through learning T2 - In Proc. SAVCBS Workshop SP - 14 KW - agdaspin KW - assume-gurantee-reasoning KW - copy KW - model-checking AU - Barringer, Howard PY - 2003/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.3.8668 ER -