%0 Conference Paper %1 1427801 %A Bobaru, Mihaela Gheorghiu %A Pasareanu, Corina S. %A Giannakopoulou, Dimitra %B CAV '08: Proceedings of the 20th international conference on Computer Aided Verification %C Berlin, Heidelberg %D 2008 %I Springer-Verlag %K abstraction_refinement assume_guarantee automated c compositional finite_state predicate_abstraction refinement safety verification %P 135--148 %R http://dx.doi.org/10.1007/978-3-540-70545-1_14 %T Automated Assume-Guarantee Reasoning by Abstraction Refinement %U http://portal.acm.org/citation.cfm?id=1427801 %X Current automated approaches for compositional model checking in the assume-guarantee style are based on learning of assumptions as deterministic automata. We propose an alternative approach based on abstraction refinement. Our new method computes the assumptions for the assume-guarantee rules as conservative and not necessarily deterministic abstractions of some of the components, and refines those abstractions using counterexamples obtained from model checking them together with the other components. Our approach also exploits the alphabets of the interfaces between components and performs iterative refinement of those alphabets as well as of the abstractions. We show experimentally that our preliminary implementation of the proposed alternative achieves similar or better performance than a previous learning-based implementation. %@ 978-3-540-70543-7

@inproceedings{1427801, abstract = {Current automated approaches for compositional model checking in the assume-guarantee style are based on learning of assumptions as deterministic automata. We propose an alternative approach based on abstraction refinement. Our new method computes the assumptions for the assume-guarantee rules as conservative and not necessarily deterministic abstractions of some of the components, and refines those abstractions using counterexamples obtained from model checking them together with the other components. Our approach also exploits the alphabets of the interfaces between components and performs iterative refinement of those alphabets as well as of the abstractions. We show experimentally that our preliminary implementation of the proposed alternative achieves similar or better performance than a previous learning-based implementation.}, added-at = {2010-01-27T11:37:57.000+0100}, address = {Berlin, Heidelberg}, author = {Bobaru, Mihaela Gheorghiu and P\u{a}s\u{a}reanu, Corina S. and Giannakopoulou, Dimitra}, biburl = {https://www.bibsonomy.org/bibtex/2813b7156794bf6c118732fdb15ae1b7a/giuliano.losa}, booktitle = {CAV '08: Proceedings of the 20th international conference on Computer Aided Verification}, description = {Automated Assume-Guarantee Reasoning by Abstraction Refinement}, doi = {http://dx.doi.org/10.1007/978-3-540-70545-1_14}, interhash = {2967fbdc4e31705b1f193871974edcbe}, intrahash = {813b7156794bf6c118732fdb15ae1b7a}, isbn = {978-3-540-70543-7}, keywords = {abstraction_refinement assume_guarantee automated c compositional finite_state predicate_abstraction refinement safety verification}, location = {Princeton, NJ, USA}, pages = {135--148}, publisher = {Springer-Verlag}, timestamp = {2010-01-27T15:13:02.000+0100}, title = {Automated Assume-Guarantee Reasoning by Abstraction Refinement}, url = {http://portal.acm.org/citation.cfm?id=1427801}, year = 2008 }