Proof Rules for Automated Compositional Verification through Learning
- Author:
- Giannakopoulou, Dimitra
- Published:
- [2003].
- Physical Description:
- 1 electronic document
- Additional Creators:
- Barringer, Howard
Pasareanu, Corina S. - Access Online:
- hdl.handle.net
- Restrictions on Access:
- Unclassified, Unlimited, Publicly available.
- Summary:
- 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 non-trivial, typically requiring human input to determine appropriate assumptions. In this paper, we present novel assume- guarantee 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.
- Collection:
- NASA Technical Reports Server (NTRS) Collection.
- Note:
- Document ID: 20030107507.
SAVBS 2003; 2003; Unknown. - Terms of Use and Reproduction:
- Copyright, Distribution as joint owner in the copyright.
- Access Online:
- hdl.handle.net
View MARC record | catkey: 15966203