{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:47:47Z","timestamp":1725551267320},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540635314"},{"type":"electronic","value":"9783540695929"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63531-9_17","type":"book-chapter","created":{"date-parts":[[2010,4,5]],"date-time":"2010-04-05T16:01:15Z","timestamp":1270483275000},"page":"227-243","source":"Crossref","is-referenced-by-count":14,"title":["Verification of liveness properties using compositional reachability analysis"],"prefix":"10.1007","author":[{"given":"Shing Chi","family":"Cheung","sequence":"first","affiliation":[]},{"given":"Dimitra","family":"Giannakopoulou","sequence":"additional","affiliation":[]},{"given":"Jeff","family":"Kramer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,8,1]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"S. Aggarwal, C. Courcoubetis, and P. Wolper, \u201cAdding Liveness Properties to Coupled Finite-State Machines,\u201d ACM Transactions on Programming Languages and Systems, vol. 12, no. 2,, 1990.","DOI":"10.1145\/78942.78948"},{"key":"17_CR2","unstructured":"A. V. Aho, J. E. Hopcroft, and J. D. Ullman, Data Structures and Algorithms: Addison-Wesley, 1983."},{"issue":"1","key":"17_CR3","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1145\/59287.62028","volume":"11","author":"B. Alpern","year":"1989","unstructured":"B. Alpern and F. B. Schneider, \u201cVerifying Temporal Properties without Temporal Logic,\u201d ACM Transactions on Programming Languages and Systems, vol. 11, no. 1, pp. 147\u2013167, 1989.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"17_CR4","unstructured":"G. R. Andrews, Concurrent Programming \u2014 Principles and Practice: The Benjamin \/ Cummings Publishing Company Ltd., 1991."},{"issue":"11","key":"17_CR5","doi-asserted-by":"crossref","first-page":"1204","DOI":"10.1109\/32.106975","volume":"17","author":"G. S. Avrunin","year":"1991","unstructured":"G. S. Avrunin, U. A. Buy, J. C. Corbett, L. K. Dillon, and J. C. Wileden, \u201cAutomated Analysis of Concurrent Systems with the Constrained Expression Toolset,\u201d IEEE Transactions on Software Engineering, vol. 17, no. 11, pp. 1204\u20131222, 1991.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"T. Bultan, J. Fischer, and R. Gerber, \u201cCompositional Verification by Model Checking for Counter-Examples,\u201d presented at International Symposium on Software Testing and Analysis, San Diego, California, January 1996.","DOI":"10.1145\/229000.226321"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"S. C. Cheung and J. Kramer, \u201cChecking Subsystem Safety Properties in Compositional Reachability Analysis,\u201d presented at 18th International Conference on Software Engineering, Berlin, Germany, March 1996.","DOI":"10.1109\/ICSE.1996.493410"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"S. C. Cheung and J. Kramer, \u201cContext Constraints for Compositional Reachability Analysis,\u201d ACM Transactions on Software Engineering and Methodology,, October 1996.","DOI":"10.1145\/235321.235323"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, D. E. Long, and K. L. McMillan, \u201cCompositional Model Checking,\u201d presented at 4th Annual Symposium on Logic in Computer Science, Pacific Grove, California, June 1989.","DOI":"10.1109\/LICS.1989.39190"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"H.-C. Fernandez, L. Mounier, C. Jard, and T. J\u00e9ron, \u201cOn-the-fly Verification of Finite Transition Systems,\u201d in Computer-Aided Verification, R. Kurshan, Ed.: Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3556-0_4"},{"key":"17_CR11","unstructured":"C. Ghezzi, M. Jazayeri, and D. Mandrioli, Fundamentals of Software Engineering, Chapter 6: Prentice-Hall, Inc., 1991."},{"key":"17_CR12","unstructured":"D. Giannakopoulou, J. Kramer, and S. C. Cheung, \u201cTRACTA: An Environment for Analysing the Behaviour of Distributed Systems,\u201d presented at ACM SIGPLAN Workshop on Automated Analysis of Software, Paris, January 1997."},{"key":"17_CR13","unstructured":"P. Godefroid and G. J. Holzmann, \u201cOn the Verification of Temporal Properties,\u201d presented at 13th IFIP WG 6.1 International Symposium, on Protocol Specification, Testing, and Verification."},{"key":"17_CR14","unstructured":"P. Gribomont and P. Wolper, \u201cTemporal Logic,\u201d in From Modal Logic to Deductive Databases, A. Thayse, Ed.: John Wiley and Sons, 1989."},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"C. A. R. Hoare, Communicating Sequential Processes: Prentice-Hall, 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"17_CR16","unstructured":"J. Kemppainen, M. Levanto, A. Valmari, and M. Clegg, \u201cARA\u201d Puts Advanced Reachability Analysis Techniques Together,\u201d presented at 5th Nordic Workshop on Programming Environment Research, Tampere, Finland, January 1992."},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"J. Kramer and J. Magee, \u201cExposing the Skeleton in the Coordination Closet,\u201d presented at Coordination `97, Berlin, September 1997.","DOI":"10.1007\/3-540-63383-9_70"},{"key":"17_CR18","unstructured":"J. C. Lin and S. Paul, \u201cRMTP: A Reliable Multicast Transport Protocol,\u201d presented at IEEE INFOCOMM'96, San Francisco, California, March 1996."},{"key":"17_CR19","unstructured":"J. Malhotra, S. A. Smolka, A. Giacalone, and R. Shapiro, \u201cA Tool for Hierarchical Design and Simulation of Concurrent Systems,\u201d presented at BCS-FACS Workshop on Specification and Verification of Concurrent Systems, Stirling, Scotland, July 1988."},{"key":"17_CR20","unstructured":"R. Milner, Communication and Concurrency: Prentice-Hall, 1989."},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"A. Rabinovich, \u201cChecking Equivalences Between Concurrent Systems of Finite Agents,\u201d presented at 19th International Colloquium on Automata, Languages and Programming, Wien, Austria, July 1992.","DOI":"10.1007\/3-540-55719-9_115"},{"issue":"9","key":"17_CR22","doi-asserted-by":"crossref","first-page":"940","DOI":"10.1109\/26.35374","volume":"37","author":"K. K. Sabnani","year":"1989","unstructured":"K. K. Sabnani, A. M. Lapone, and M. U. Uyar, \u201cAn Algorithmic Procedure for Checking Safety Properties of Protocols,\u201d IEEE Transactions on Communications, vol. 37, no. 9, pp. 940\u2013948, September 1989.","journal-title":"IEEE Transactions on Communications"},{"key":"17_CR23","unstructured":"K. C. Tai and P. V. Koppol, \u201cHierarchy-Based Incremental Reachability Analysis of Communication Protocols,\u201d presented at IEEE International Conference on Network Protocols, San Francisco, California, October 1993."},{"key":"17_CR24","unstructured":"A. Valmari. Alleviating State Explosion during Verification of Behavioural Equivalence, Technical Report, A-1992, Department of Computer Science, University of Helsinki, Finland, August 1992."},{"key":"17_CR25","unstructured":"W. J. Yeh. Controlling State Explosion in Reachability Analysis, Technical Report, SERC-TR-147-P, SERC, Purdue University, December 1993."},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"W. J. Yeh and M. Young, \u201cCompositional Reachability Analysis Using Process Algebra,\u201d presented at Symposium on Testing, Analysis, and Verification (TAV4), Victoria, British Columbia, October 8\u201310, 1991.","DOI":"10.1145\/120807.120812"},{"key":"17_CR27","unstructured":"W. J. Yeh and M. Young, \u201cHierarchical Tracing of Concurrent Programs,\u201d presented at 3rd Irvine Software Symposium (ISS'93), Irvine, California, April 1993."}],"container-title":["Lecture Notes in Computer Science","Software Engineering \u2014 ESEC\/FSE'97"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63531-9_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,31]],"date-time":"2023-05-31T14:25:28Z","timestamp":1685543128000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63531-9_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540635314","9783540695929"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-63531-9_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}