{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:51:22Z","timestamp":1725573082797},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540242970"},{"type":"electronic","value":"9783540305798"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-30579-8_30","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T16:45:34Z","timestamp":1292863534000},"page":"465-481","source":"Crossref","is-referenced-by-count":16,"title":["Efficiently Verifiable Conditions for Deadlock-Freedom of Large Concurrent Programs"],"prefix":"10.1007","author":[{"given":"Paul C.","family":"Attie","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hana","family":"Chockler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"30_CR1","doi-asserted-by":"crossref","unstructured":"Aldini, A., Bernardo, M.: A general approach to deadlock freedom verification for software architectures. In: FM 2003. LNCS, vol.\u00a02805, pp. 658\u2013677 (2003)","DOI":"10.1007\/978-3-540-45236-2_36"},{"key":"30_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Computer Aided Verification","author":"T. Arons","year":"2001","unstructured":"Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.D.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 221\u2013234. Springer, Heidelberg (2001)"},{"key":"30_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/3-540-48320-9_11","volume-title":"CONCUR\u201999. Concurrency Theory","author":"P.C. Attie","year":"1999","unstructured":"Attie, P.C.: Synthesis of large concurrent programs via pairwise composition. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, p. 130. Springer, Heidelberg (1999)"},{"issue":"1","key":"30_CR4","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1145\/271510.271519","volume":"20","author":"P.C. Attie","year":"1998","unstructured":"Attie, P.C., Emerson, E.A.: Synthesis of concurrent systems with many similar processes. ACM Trans. Program. Lang. Syst.\u00a020(1), 51\u2013115 (1998)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"30_CR5","unstructured":"Attie, P.C.: Synthesis of large dynamic concurrent programs from dynamic specifications. Technical report, NEU, Boston, MA (2003)"},{"key":"30_CR6","unstructured":"Attie, P.C.: Finite-state concurrent programs can be expressed pairwise. Technical report, NEU, Boston, MA (2004)"},{"key":"30_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without bDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"30_CR8","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"30_CR9","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. FMSD\u00a09(2) (1996)","DOI":"10.1007\/BF00625969"},{"key":"30_CR10","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1145\/356586.356588","volume":"3","author":"E.G. Coffman","year":"1971","unstructured":"Coffman, E.G., Elphick, M.J., Shoshani, A.: System deadlocks. ACM Comput. Surv.\u00a03, 67\u201378 (1971)","journal-title":"ACM Comput. Surv."},{"key":"30_CR11","volume-title":"Introduction to Algorithms","author":"T.H. Cormen","year":"2001","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 2nd edn. MIT Press and McGraw-Hill, Cambridge (2001)","edition":"2"},{"key":"30_CR12","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall Inc., Englewood Cliffs (1976)"},{"key":"30_CR13","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: CAD, pp. 236\u2013254 (2000)","DOI":"10.1007\/10721959_19"},{"issue":"1\/2","key":"30_CR14","first-page":"105","volume":"9","author":"E.A. Emerson","year":"1996","unstructured":"Emerson, E.A., Prasad Sistla, A.: Symmetry and model checking. FMSD\u00a09(1\/2), 105\u2013131 (1996)","journal-title":"FMSD"},{"key":"30_CR15","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E.A. Emerson","year":"1982","unstructured":"Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program.\u00a02, 241\u2013266 (1982)","journal-title":"Sci. Comput. Program."},{"key":"30_CR16","unstructured":"Godefroid, P.: Partial Order Methods for the Verification of Concurrent Systems. PhD thesis, University of Liege (1994)"},{"issue":"7","key":"30_CR17","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1109\/32.538606","volume":"22","author":"P. Godefroid","year":"1996","unstructured":"Godefroid, P., Peled, D., Staskauskas, M.: Using partial-order methods in the formal validation of industrial concurrent programs. Trans. on Soft. Eng.\u00a022(7), 496\u2013507 (1996)","journal-title":"Trans. on Soft. Eng."},{"issue":"2","key":"30_CR18","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1006\/inco.1994.1035","volume":"110","author":"P. Godefroid","year":"1991","unstructured":"Godefroid, P., Wolper, P.: A partial approach to model checking. Information and Computation\u00a0110(2), 305\u2013326 (1991)","journal-title":"Information and Computation"},{"key":"30_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-540-24597-1_36","volume-title":"FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science","author":"G. Goessler","year":"2003","unstructured":"Goessler, G., Sifakis, J.: Component-Based Construction of Deadlock-Free Systems. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol.\u00a02914, pp. 420\u2013433. Springer, Heidelberg (2003)"},{"issue":"3","key":"30_CR20","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1145\/356603.356607","volume":"4","author":"R.C. Holt","year":"1972","unstructured":"Holt, R.C.: Some deadlock properties of computer systems. ACM Comput. Surv.\u00a04(3), 179\u2013196 (1972)","journal-title":"ACM Comput. Surv."},{"key":"30_CR21","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic Model Checking: 1020 States and Beyond. In: LICS, pp. 1\u201333 (1990)"},{"issue":"4","key":"30_CR22","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1145\/45075.46163","volume":"19","author":"E. Knapp","year":"1987","unstructured":"Knapp, E.: Deadlock detection in distributed databases. ACM Comput. Surv.\u00a019(4), 303\u2013328 (1987)","journal-title":"ACM Comput. Surv."},{"key":"30_CR23","doi-asserted-by":"crossref","unstructured":"Ladkin, P., Simons, B.: Compile-time analysis of communicating processes. In: Proc. Int. Conf. on Supercomputing, pp. 248\u2013259 (1992)","DOI":"10.1145\/143369.143417"},{"key":"30_CR24","volume-title":"Distributed Algorithms","author":"N.A. Lynch","year":"1996","unstructured":"Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1996)"},{"key":"30_CR25","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"30_CR26","doi-asserted-by":"crossref","unstructured":"Peled, D.: Partial order reduction: Model-checking using representatives. In: MFCS (1996)","DOI":"10.1007\/3-540-61550-4_141"},{"key":"30_CR27","unstructured":"Rex, B.: Inference of k-process behavior from two-process programs. Master\u2019s thesis, School of Computer Science, Florida International University, Miami, FL (April 1999)"},{"key":"30_CR28","volume-title":"Modern Operating Systems","author":"A.S. Tanenbaum","year":"2001","unstructured":"Tanenbaum, A.S.: Modern Operating Systems, 2nd edn. Prentice-Hall, Englewood Cliffs (2001)","edition":"2"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30579-8_30.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:24:19Z","timestamp":1605759859000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30579-8_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540242970","9783540305798"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30579-8_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}