{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T15:41:40Z","timestamp":1759333300254},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664994"},{"type":"electronic","value":"9783540482345"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48234-2_14","type":"book-chapter","created":{"date-parts":[[2007,10,29]],"date-time":"2007-10-29T23:58:10Z","timestamp":1193702290000},"page":"168-183","source":"Crossref","is-referenced-by-count":33,"title":["Assume-Guarantee Model Checking of Software: A Comparative Case Study"],"prefix":"10.1007","author":[{"given":"Corina S.","family":"P\u0103s\u0103reanu","sequence":"first","affiliation":[]},{"given":"Matthew B.","family":"Dwyer","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Huth","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,8,27]]},"reference":[{"issue":"1","key":"14_CR1","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/151646.151649","volume":"15","author":"A. M","year":"1993","unstructured":"M. Abadi and L. Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems, 15(1):73\u2013132, January 1993.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1","key":"14_CR2","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/32.210305","volume":"19","author":"A. J","year":"1993","unstructured":"J. Atlee and J. Gannon. State-based model checking of event-driven system requirements. IEEE Transactions on Software Engineering, 19(1):24\u201340, June 1993.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"G.S. Avrunin, J.C. Corbett, and L.K. Dillon. Analyzing partially-implemented real-time systems. In Proceedings of the 19th International Conference on Software Engineering, May 1997.","DOI":"10.1145\/253228.253275"},{"key":"14_CR4","unstructured":"A.T. Chamillard. An Empirical Comparison of Static Concurrency Analysis Techniques. PhD thesis, University of Massachusetts at Amherst, May 1996."},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"S.C. Cheung and J. Kramer. Checking subsystem safety properties in compositional reachability analysis. In Proceedings of the 18th International Conference on Software Engineering, Berlin, March 1996.","DOI":"10.1109\/ICSE.1996.493410"},{"issue":"2","key":"14_CR6","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, April 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"J.C. Corbett. Evaluating deadlock detection methods for concurrent software.IEEE Transactions on Software Engineering, 22(3), March 1996.","DOI":"10.1109\/32.489078"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM Symposium on Principles of Programming Languages, pages 238\u2013252, 1977.","DOI":"10.1145\/512950.512973"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"M.B. Dwyer and C.S. P-as-areanu. Filter-based model checking of partial systems. In Proceedings of the Sixth ACM SIGSOFT Symposium on Foundations of Software Engineering, November 1998.","DOI":"10.1145\/288195.288307"},{"key":"14_CR10","series-title":"Lect Notes Comput Sci","volume-title":"Generic Programing: Proceedings of a Dagstuhl Seminar","author":"M.B. Dwyer","year":"1998","unstructured":"M.B. Dwyer and C.S. P-as-areanu. Model checking generic container implementations. In Generic Programing: Proceedings of a Dagstuhl Seminar, Lecture Notes in Computer Science, Dagstuhl Castle, Germany, 1998. to appear. Assume-Guarantee Model Checking of Software: A Comparative Case Study 183"},{"key":"14_CR11","unstructured":"M.B. Dwyer, C.S. P-as-areanu, and J.C. Corbett. Translating ada programs for model checking: A tutorial. Technical Report 98-12, Kansas State University, Department of Computing and Information Sciences, 1998."},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"M.B. Dwyer, G.S. Avrunin, and J.C. Corbett. Patterns in property specifications for finite-state verification. In Proceedings of the 21st International Conference on Software Engineering, May 1999.","DOI":"10.1145\/302405.302672"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"R. Gerth, D. Peled, M.Y. Vardi, and P. Wolper. Simple On-the-fly Automatic Verification of Linear Temporal Logic. In Proceedings of PSTV\u201995, 1995.","DOI":"10.1007\/978-0-387-34892-6_1"},{"issue":"3","key":"14_CR14","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"O. Grumberg and D.E. Long. Model Checking and Modular Verification. ACM Transactions on Programming Languages and Systems, 16(3):843\u2013871, May 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"K. Havelund and T. Pressburger.Model checking java programs using java pathfinder. International Journal on Software Tools for Technology Transfer, 1999.to appear.","DOI":"10.1007\/s100090050043"},{"issue":"5","key":"14_CR16","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"G.J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279\u2013294, May 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"14_CR17","unstructured":"R. Iosef. A concurrency analysis tool for java programs. Master\u2019s thesis, Polytechnic University of Turin, August 1997."},{"key":"14_CR18","unstructured":"N.D. Jones, C.K. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice-Hall International, 1993."},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"O. Kupferman and M.Y. Vardi. On the complexity of branching modular model checking (extended abstract). In Insup Lee and Scott A. Smolka, editors, CONCUR\u2019 95: Concurrency Theory, 6th International Conference, volume 962 of Lecture Notes in Computer Science, pages 408\u2013422, Philadelphia, Pennsylvania, 21-24 August 1995. Springer-Verlag.","DOI":"10.1007\/3-540-60218-6_31"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems Specification. Springer-Verlag, 1991.","DOI":"10.1007\/978-1-4612-0931-7"},{"issue":"1","key":"14_CR21","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/357233.357237","volume":"6","author":"M. Z","year":"1984","unstructured":"Z. Manna and P. Wolper. Synthesis of communicating processes from temporal logic. ACM Transactions on Programming Languages and Systems (TOPLAS), 6(1):68\u201393, 1984.","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"G.N. Naumovich, G.S. Avrunin, L.A. Clarke, and L.J. Osterweil. Applying static analysis to software architectures. In LNCS 1301. The 6th European Software Engineering Conference held jointly with the 5th ACM SIGSOFT Symposium on the Foundations of Software Engineering, September 1997.","DOI":"10.1007\/3-540-63531-9_8"},{"key":"14_CR24","unstructured":"C.S. P-as-areanu, M.B. Dwyer, and M. Huth. Modular Verification of Software Units. Technical Report 98-15, Kansas State University, Department of Computing and Information Sciences, 1998."},{"key":"14_CR25","unstructured":"C.S. P-as-areanu and M.B. Dwyer. Software Model Checking Case Studies. http:\/\/www.cis.ksu.edu\/santos\/bandera\/index.html#case-studies , 1998."},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"A. Pnueli. In transition from global to modular temporal reasoning about programs. In K. Apt, editor, Logics and Models of Concurrent Systems, pages 123\u2013144. Springer-Verlag, 1985.","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"14_CR27","doi-asserted-by":"crossref","unstructured":"M.Y. Vardi. On the complexity of modular model checking. In Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science, pages 101\u2013111, San Diego, California, 26-29 June 1995. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1995.523248"},{"key":"14_CR28","doi-asserted-by":"crossref","unstructured":"P. Wolper. Specifying interesting properties of programs in propositional temporal logics. In Proceedings of the 13th ACM Symposium on Principles of Programming Languages, pages 184\u2013193, St. Petersburg, Fla., January 1986.","DOI":"10.1145\/512644.512661"},{"issue":"1","key":"14_CR29","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1145\/201055.201080","volume":"4","author":"M. Young","year":"1995","unstructured":"M. Young, R.N. Taylor, D.L. Levine, K.A. Nies, and D. Brodbeck. A concurrency analysis tool suite: Rationale, design, and preliminary experience. ACM Transactions on Software Engineering and Methodology, 4(1):64\u2013106, January 1995.","journal-title":"ACM Transactions on Software Engineering and Methodology"}],"container-title":["Lecture Notes in Computer Science","Theoretical and Practical Aspects of SPIN Model Checking"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48234-2_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T23:15:43Z","timestamp":1556925343000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48234-2_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664994","9783540482345"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-48234-2_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}