{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T04:37:21Z","timestamp":1725856641385},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319336923"},{"type":"electronic","value":"9783319336930"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-33693-0_22","type":"book-chapter","created":{"date-parts":[[2016,5,24]],"date-time":"2016-05-24T01:35:47Z","timestamp":1464053747000},"page":"345-360","source":"Crossref","is-referenced-by-count":11,"title":["Efficient Deadlock-Freedom Checking Using Local Analysis and SAT Solving"],"prefix":"10.1007","author":[{"given":"Pedro","family":"Antonino","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Gibson-Robinson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A. W.","family":"Roscoe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,5,24]]},"reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/978-3-319-06200-6_3","volume-title":"NASA Formal Methods","author":"PRG Antonino","year":"2014","unstructured":"Antonino, P.R.G., Oliveira, M.M., Sampaio, A.C.A., Kristensen, K.E., Bryans, J.W.: Leadership election:\u00a0an industrial SoS application of compositional deadlock verification. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 31\u201345. Springer, Heidelberg (2014)"},{"key":"22_CR2","unstructured":"Antonino, P., Roscoe, A.W., Gibson-Robinson, T.: Experiment package (2015). http:\/\/www.cs.ox.ac.uk\/people\/pedro.antonino\/exp.zip"},{"key":"22_CR3","unstructured":"Antonino, P., Roscoe, A.W., Gibson-Robinson, T.: Efficient deadlock analysis using local analysis and SAT solving. Technical report, University of Oxford (2015). http:\/\/www.cs.ox.ac.uk\/people\/pedro.antonino\/techreport.pdf"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/978-3-319-06410-9_5","volume-title":"FM 2014: Formal Methods","author":"P Antonino","year":"2014","unstructured":"Antonino, P., Sampaio, A., Woodcock, J.: A refinement based strategy for local deadlock analysis of networks of CSP processes. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 62\u201377. Springer, Switzerland (2014)"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/978-3-642-38592-6_12","volume-title":"Formal Techniques for Distributed Systems","author":"PC Attie","year":"2013","unstructured":"Attie, P.C., Bensalem, S., Bozga, M., Jaber, M., Sifakis, J., Zaraket, F.A.: An abstract framework for deadlock prevention in BIP. In: Beyer, D., Boreale, M. (eds.) FMOODS\/FORTE 2013. LNCS, vol. 7892, pp. 161\u2013177. Springer, Heidelberg (2013)"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1007\/978-3-540-30579-8_30","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"PC Attie","year":"2005","unstructured":"Attie, P.C., Chockler, H.: Efficiently verifiable conditions for deadlock-freedom of large concurrent programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 465\u2013481. Springer, Heidelberg (2005)"},{"key":"22_CR7","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: IJCAI 2009, San Francisco, CA, USA, pp. 399\u2013404 (2009)"},{"key":"22_CR8","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/BF01784721","volume":"4","author":"SD Brookes","year":"1991","unstructured":"Brookes, S.D., Roscoe, A.W.: Deadlock analysis in networks of communicating processes. Distrib. Comput. 4, 209\u2013230 (1991)","journal-title":"Distrib. Comput."},{"issue":"2","key":"22_CR9","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1145\/356586.356588","volume":"3","author":"EG Coffman","year":"1971","unstructured":"Coffman, E.G., Elphick, M., Shoshani, A.: System deadlocks. ACM Comput. Surv. (CSUR) 3(2), 67\u201378 (1971)","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/978-3-642-54862-8_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Gibson-Robinson","year":"2014","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 \u2014 a modern refinement checker for CSP. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 187\u2013201. Springer, Heidelberg (2014)"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1007\/978-3-319-17524-9_14","volume-title":"NASA Formal Methods","author":"T Gibson-Robinson","year":"2015","unstructured":"Gibson-Robinson, T., Hansen, H., Roscoe, A.W., Wang, X.: Practical partial order reduction for CSP. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 188\u2013203. Springer, Switzerland (2015)"},{"issue":"2","key":"22_CR12","first-page":"149","volume":"2","author":"P Godefroid","year":"1993","unstructured":"Godefroid, P., Wolper, P.: Using partial orders for the efficient verification of deadlock freedom and safety properties. FMSD 2(2), 149\u2013164 (1993)","journal-title":"FMSD"},{"key":"22_CR13","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1007\/978-3-642-29320-7_5","volume-title":"Fundamentals of Software Engineering","author":"C Lambertz","year":"2012","unstructured":"Lambertz, C., Majster-Cederbaum, M.: Analyzing component-based systems on the basis of architectural constraints. In: Arbab, F., Sirjani, M. (eds.) FSEN 2011. LNCS, vol. 7141, pp. 64\u201379. Springer, Heidelberg (2012)"},{"key":"22_CR15","unstructured":"Martin, J.M.R.: The design and construction of deadlock-free concurrent systems. Ph.D. thesis, University of Buckingham (1996)"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"418","DOI":"10.1007\/3-540-63533-5_22","volume-title":"FME \u201997: Industrial Applications and Strengthened Foundations of Formal Methods","author":"JMR Martin","year":"1997","unstructured":"Martin, J.M.R., Jassim, S.A.: An efficient technique for deadlock analysis of large scale process networks. In: Fitzgerald, J., Jones, C.B., Lucas, P. (eds.) FME 1997. LNCS, vol. 1313, pp. 418\u2013441. Springer, Heidelberg (1997)"},{"issue":"3","key":"22_CR17","first-page":"1","volume":"9","author":"J Ouaknine","year":"2013","unstructured":"Ouaknine, J., Palikareva, H., Roscoe, A.W., Worrell, J.: A static analysis framework for livelock freedom in CSP. LMCS 9(3), 1\u201353 (2013)","journal-title":"LMCS"},{"issue":"3","key":"22_CR18","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1016\/0890-5401(87)90004-6","volume":"75","author":"AW Roscoe","year":"1987","unstructured":"Roscoe, A.W., Dathi, N.: The pursuit of deadlock freedom. Inf. Comput. 75(3), 289\u2013327 (1987)","journal-title":"Inf. Comput."},{"key":"22_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/3-540-60630-0_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"AW Roscoe","year":"1995","unstructured":"Roscoe, A.W., Gardiner, P.H.B., Goldsmith, M.H., Hulance, J.R., Jackson, D.M., Scattergood, J.B.: Hierarchical compression for model-checking CSP or how to check 10 $$^{20}$$ 20 dining philosophers for deadlock. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 133\u2013152. Springer, Heidelberg (1995)"},{"key":"22_CR20","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-84882-258-0","volume-title":"Understanding Concurrent Systems","author":"AW Roscoe","year":"2010","unstructured":"Roscoe, A.W.: Understanding Concurrent Systems. Springer, London (2010)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-33693-0_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T10:43:53Z","timestamp":1498301033000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-33693-0_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319336923","9783319336930"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-33693-0_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}