{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:41:40Z","timestamp":1750308100655,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":17,"publisher":"ACM","license":[{"start":{"date-parts":[[2005,11,7]],"date-time":"2005-11-07T00:00:00Z","timestamp":1131321600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2005,11,7]]},"DOI":"10.1145\/1101908.1101974","type":"proceedings-article","created":{"date-parts":[[2006,2,6]],"date-time":"2006-02-06T15:52:40Z","timestamp":1139241160000},"page":"376-379","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Compositional reasoning for port-based distributed systems"],"prefix":"10.1145","author":[{"given":"Alma L.","family":"Juarez Dominguez","sequence":"first","affiliation":[{"name":"University of Waterloo, Waterloo, ON, Canada"}]},{"given":"Nancy A.","family":"Day","sequence":"additional","affiliation":[{"name":"University of Waterloo, Waterloo, ON, Canada"}]}],"member":"320","published-online":{"date-parts":[[2005,11,7]]},"reference":[{"key":"e_1_3_2_1_1_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/3-540-48153-2_7","volume-title":"Correct Hardware Design and Verification Methods","author":"Amla N.","year":"1999","unstructured":"N. Amla , E. A. Emerson , and K. S. Namjoshi . Efficient decompositional model-checking for regular timing diagrams . In Correct Hardware Design and Verification Methods , volume 1703 of LNCS , pages 67 -- 81 , 1999 .]] N. Amla, E. A. Emerson, and K. S. Namjoshi. Efficient decompositional model-checking for regular timing diagrams. In Correct Hardware Design and Verification Methods, volume 1703 of LNCS, pages 67--81, 1999.]]"},{"key":"e_1_3_2_1_2_1","first-page":"49","volume-title":"IP-Telephony Workshop","author":"Bond G.","year":"2001","unstructured":"G. Bond , F. Ivanci\u0106 , N. Klarlund , and R. Trefler . ECLIPSE feature logic analysis . IP-Telephony Workshop , pages 49 -- 56 , 2001 .]] G. Bond, F. Ivanci\u0106, N. Klarlund, and R. Trefler. ECLIPSE feature logic analysis. IP-Telephony Workshop, pages 49--56, 2001.]]"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/322374.322380"},{"key":"e_1_3_2_1_4_1","first-page":"49","volume-title":"International Conference on Very Large Scale Integration (VLSI)","author":"Burch J.","year":"1991","unstructured":"J. Burch , E. Clarke , and D. Long . Symbolic model checking with partitioned transition relations . In International Conference on Very Large Scale Integration (VLSI) , pages 49 -- 58 . IFIP Trans., North-Holland , 1991 .]] J. Burch, E. Clarke, and D. Long. Symbolic model checking with partitioned transition relations. In International Conference on Very Large Scale Integration (VLSI), pages 49--58. IFIP Trans., North-Holland, 1991.]]"},{"key":"e_1_3_2_1_5_1","first-page":"188","volume-title":"Int'l Conf. on Impl. and Application of Automata, number 2759 in LNCS","author":"Fu X.","year":"2003","unstructured":"X. Fu , T. Bultan , and J. Su . Conversation protocols: A formalism for specification and verification of reactive electronic services . In Int'l Conf. on Impl. and Application of Automata, number 2759 in LNCS , pages 188 -- 200 . Springer , 2003 .]] X. Fu, T. Bultan, and J. Su. Conversation protocols: A formalism for specification and verification of reactive electronic services. In Int'l Conf. on Impl. and Application of Automata, number 2759 in LNCS, pages 188--200. Springer, 2003.]]"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/155278"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177725"},{"key":"e_1_3_2_1_8_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"440","DOI":"10.1007\/BFb0028765","volume-title":"Computer-Aided Verification","author":"Henzinger T.","year":"1998","unstructured":"T. Henzinger , S. Qadeer , and S. Rajamani . You assume, we guarantee: Methodology and case studies . In Computer-Aided Verification , volume 1427 of LNCS , pages 440 -- 451 . Springer-Verlag , 1998 .]] T. Henzinger, S. Qadeer, and S. Rajamani. You assume, we guarantee: Methodology and case studies. In Computer-Aided Verification, volume 1427 of LNCS, pages 440--451. Springer-Verlag, 1998.]]"},{"key":"e_1_3_2_1_9_1","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"Holzmann G. J.","year":"2003","unstructured":"G. J. Holzmann . The Spin Model Checker: Primer and Reference Manual . Addison-Wesley , 2003 .]] G. J. Holzmann. The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, 2003.]]"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.729683"},{"key":"e_1_3_2_1_11_1","volume-title":"Nov.","author":"Jackson M.","year":"2003","unstructured":"M. Jackson and P. Zave . The DFC Manual. AT&T Labs , Nov. 2003 .]] M. Jackson and P. Zave. The DFC Manual. AT&T Labs, Nov. 2003.]]"},{"key":"e_1_3_2_1_12_1","volume-title":"School of Computer Science","author":"Juarez Dominguez A. L.","year":"2005","unstructured":"A. L. Juarez Dominguez . Verification of DFC call protocol correctness criteria. Master's thesis , School of Computer Science , University of Waterloo . May , 2005 .]] A. L. Juarez Dominguez. Verification of DFC call protocol correctness criteria. Master's thesis, School of Computer Science, University of Waterloo. May, 2005.]]"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/581771.581775"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/3-540-48153-2_17","volume-title":"Correct Hardware Design and Verification Methods, number 1703 in LNCS","author":"McMillan K. L.","year":"1999","unstructured":"K. L. McMillan . Verification of infinite state systems by compositional model checking . In Correct Hardware Design and Verification Methods, number 1703 in LNCS , pages 219 -- 233 . Springer , 1999 .]] K. L. McMillan. Verification of infinite state systems by compositional model checking. In Correct Hardware Design and Verification Methods, number 1703 in LNCS, pages 219--233. Springer, 1999.]]"},{"key":"e_1_3_2_1_15_1","first-page":"123","volume-title":"transition from global to modular temporal reasoning about programs. In Logic and models of concurrent systems","author":"Pnueli A.","year":"1985","unstructured":"A. Pnueli . In transition from global to modular temporal reasoning about programs. In Logic and models of concurrent systems , pages 123 -- 144 . Springer , 1985 .]] A. Pnueli. In transition from global to modular temporal reasoning about programs. In Logic and models of concurrent systems, pages 123--144. Springer, 1985.]]"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30482-1_26"},{"key":"e_1_3_2_1_17_1","first-page":"395","volume-title":"19th International NATO Summer School: Calculational System Design","author":"Zave P.","year":"1999","unstructured":"P. Zave . Formal description of telecommunication services in Promela and Z . In 19th International NATO Summer School: Calculational System Design , pages 395 -- 420 , 1999 .]] P. Zave. Formal description of telecommunication services in Promela and Z. In 19th International NATO Summer School: Calculational System Design, pages 395--420, 1999.]]"}],"event":{"name":"ASE05: International Conference on Automated Software Engineering 2005","sponsor":["SIGAI ACM Special Interest Group on Artificial Intelligence","ACM Association for Computing Machinery","SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Long Beach CA USA","acronym":"ASE05"},"container-title":["Proceedings of the 20th IEEE\/ACM International Conference on Automated Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1101908.1101974","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1101908.1101974","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:08:02Z","timestamp":1750262882000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1101908.1101974"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,11,7]]},"references-count":17,"alternative-id":["10.1145\/1101908.1101974","10.1145\/1101908"],"URL":"https:\/\/doi.org\/10.1145\/1101908.1101974","relation":{},"subject":[],"published":{"date-parts":[[2005,11,7]]},"assertion":[{"value":"2005-11-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}