{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T08:52:59Z","timestamp":1743151979766,"version":"3.40.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319708478"},{"type":"electronic","value":"9783319708485"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-70848-5_15","type":"book-chapter","created":{"date-parts":[[2017,11,10]],"date-time":"2017-11-10T10:43:26Z","timestamp":1510310606000},"page":"233-250","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Checking Static Properties Using Conservative SAT Approximations for Reachability"],"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":[[2017,11,11]]},"reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-662-54580-5_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Antonino","year":"2017","unstructured":"Antonino, P., Gibson-Robinson, T., Roscoe, A.W.: The automatic detection of token structures and invariants using SAT checking. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 249\u2013265. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_15"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-319-33693-0_22","volume-title":"Integrated Formal Methods","author":"P Antonino","year":"2016","unstructured":"Antonino, P., Gibson-Robinson, T., Roscoe, A.W.: Efficient deadlock-freedom checking using local analysis and SAT solving. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 345\u2013360. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33693-0_22"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-319-48989-6_3","volume-title":"FM 2016: Formal Methods","author":"P Antonino","year":"2016","unstructured":"Antonino, P., Gibson-Robinson, T., Roscoe, A.W.: Tighter reachability criteria for deadlock-freedom analysis. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 43\u201359. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_3"},{"key":"15_CR4","unstructured":"Antonino, P., Gibson-Robinson, T., Roscoe, A.W.: Experiment package (2017). www.cs.ox.ac.uk\/people\/pedro.antonino\/sppkg.zip"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06200-6_3"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_5"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/978-3-642-38592-6_12"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/978-3-540-30579-8_30"},{"key":"15_CR9","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: IJCAI 2009, San Francisco, CA, USA, pp. 399\u2013404 (2009)"},{"issue":"2","key":"15_CR10","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1007\/s10270-014-0410-8","volume":"15","author":"S Bensalem","year":"2016","unstructured":"Bensalem, S., Bozga, M., Legay, A., Nguyen, T.-H., Sifakis, J., Yan, R.: Component-based verification using incremental design and invariants. Softw. Syst. Model. 15(2), 427\u2013451 (2016)","journal-title":"Softw. Syst. Model."},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-319-47846-3_18","volume-title":"Formal Methods and Software Engineering","author":"MSC Filho","year":"2016","unstructured":"Filho, M.S.C., Oliveira, M.V.M., Sampaio, A., Cavalcanti, A.: Local livelock analysis of component-based models. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 279\u2013295. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47846-3_18"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_13"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_14"},{"key":"15_CR14","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/978-3-642-29320-7_5"},{"key":"15_CR16","unstructured":"Martin, J.M.R.: The Design and Construction of Deadlock-Free Concurrent Systems. Ph.D. thesis, University of Buckingham (1996)"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/3-540-63533-5_22"},{"issue":"6","key":"15_CR18","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1007\/s00165-016-0375-1","volume":"28","author":"MVM Oliveira","year":"2016","unstructured":"Oliveira, M.V.M., Antonino, P., Ramos, R., Sampaio, A., Mota, A., Roscoe, A.W.: Rigorous development of component-based systems using component metadata and patterns. Formal Aspects Comput. 28(6), 937\u20131004 (2016). https:\/\/doi.org\/10.1007\/s00165-016-0375-1 . ISSN:1433-299X","journal-title":"Formal Aspects Comput."},{"key":"15_CR19","doi-asserted-by":"publisher","unstructured":"Ouaknine, J., Palikareva, H., Roscoe, A.W., Worrell, J.: A static analysis framework for livelock freedom in CSP. Logical Methods Comput. Sci. 9(3) September 2013. https:\/\/doi.org\/10.2168\/LMCS-9(3:24)2013","DOI":"10.2168\/LMCS-9(3:24)2013"},{"issue":"1","key":"15_CR20","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1145\/58564.59295","volume":"7","author":"K Raymond","year":"1989","unstructured":"Raymond, K.: A tree-based algorithm for distributed mutual exclusion. ACM Trans. Comput. Syst. (TOCS) 7(1), 61\u201377 (1989)","journal-title":"ACM Trans. Comput. Syst. (TOCS)"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W., Gardiner, P.H.B., Goldsmith, M., Hulance, J.R., Jackson, D.M., Scattergood, J.B.: Hierarchical compression for model-checking CSP or how to check 10 $$^{\\text{20}}$$ dining philosophers for deadlock. In: TACAS, pp. 133\u2013152 (1995)","DOI":"10.1007\/3-540-60630-0_7"},{"key":"15_CR22","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, Heidelberg (2010)"},{"key":"15_CR23","first-page":"187","volume":"14","author":"G Tarry","year":"1895","unstructured":"Tarry, G.: Le probleme des labyrinthes. Nouvelles annales de math\u00e9matiques, journal des candidats aux \u00e9coles polytechnique et normale 14, 187\u2013190 (1895)","journal-title":"Nouvelles annales de math\u00e9matiques, journal des candidats aux \u00e9coles polytechnique et normale"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-70848-5_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,5]],"date-time":"2019-10-05T20:37:09Z","timestamp":1570307829000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-70848-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319708478","9783319708485"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-70848-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}