{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T20:06:42Z","timestamp":1743106002085,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662545799"},{"type":"electronic","value":"9783662545805"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/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-662-54580-5_15","type":"book-chapter","created":{"date-parts":[[2017,3,30]],"date-time":"2017-03-30T06:50:09Z","timestamp":1490856609000},"page":"249-265","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["The Automatic Detection of Token Structures and Invariants Using SAT Checking"],"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,3,31]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Agerwala, T., Choed-Amphai, Y.-C.: A synthesis rule for concurrent systems. In: 15th Conference on Design Automation, pp. 305\u2013311. IEEE (1978)","DOI":"10.1109\/DAC.1978.1585190"},{"key":"15_CR2","unstructured":"Antonino, P., Gibson-Robinson, T., Roscoe, A.W.: Experiment package (2016). http:\/\/www.cs.ox.ac.uk\/people\/pedro.antonino\/pkg-vt.zip"},{"key":"15_CR3","unstructured":"Antonino, P., Gibson-Robinson, T., Roscoe, A.W.: The automatic detection of token structures and invariants using SAT checking. Technical report, University of Oxford (2016). http:\/\/www.cs.ox.ac.uk\/people\/pedro.antonino\/techreport-vt.pdf"},{"key":"15_CR4","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, Heidelberg (2016). doi:10.1007\/978-3-319-33693-0_22"},{"key":"15_CR5","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, Heidelberg (2016). doi:10.1007\/978-3-319-48989-6_3"},{"key":"15_CR6","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: an 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). doi:10.1007\/978-3-319-06200-6_3"},{"key":"15_CR7","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, Heidelberg (2014). doi:10.1007\/978-3-319-06410-9_5"},{"key":"15_CR8","unstructured":"Apt, K.R., Francez, N., de Roever, W.P.: A proof system for communicating sequential processes. ACM Trans. Program. Lang. Syst. (TOPLAS) 2(3), 359\u2013385 (1980)"},{"key":"15_CR9","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). doi:10.1007\/978-3-642-38592-6_12"},{"key":"15_CR10","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). doi:10.1007\/978-3-540-30579-8_30"},{"key":"15_CR11","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":"15_CR12","doi-asserted-by":"crossref","unstructured":"Batcher, K.E.: Sorting networks and their applications. In: Proceedings of the April 30-May 2, Spring Joint Computer Conference, AFIPS 1968 (Spring), pp. 307\u2013314. ACM, New York (1968)","DOI":"10.1145\/1468075.1468121"},{"issue":"1","key":"15_CR13","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1023\/A:1008744030390","volume":"15","author":"S Bensalem","year":"1999","unstructured":"Bensalem, S., Lakhnech, Y.: Automatic generation of invariants. Form. Methods Syst. Des. 15(1), 75\u201392 (1999)","journal-title":"Form. Methods Syst. Des."},{"issue":"1\u20134","key":"15_CR14","first-page":"1","volume":"2","author":"N E\u00e9n","year":"2006","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating pseudo-boolean constraints into SAT. JSAT 2(1\u20134), 1\u201326 (2006)","journal-title":"JSAT"},{"key":"15_CR15","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). doi:10.1007\/978-3-642-54862-8_13"},{"key":"15_CR16","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, Heidelberg (2015). doi:10.1007\/978-3-319-17524-9_14"},{"key":"15_CR17","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":"15_CR18","unstructured":"Jezequel, L., Lime, D.: Lazy reachability analysis in distributed systems. In: 27th International Conference on Concurrency Theory, CONCUR 2016, 23-26 August 2016, Quebec City, Canada, pp. 17:1\u201317:14 (2016)"},{"key":"15_CR19","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). doi:10.1007\/978-3-642-29320-7_5"},{"key":"15_CR20","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"2","author":"L Lamport","year":"1977","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 2, 125\u2013143 (1977)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"15_CR21","unstructured":"Martin, J.M.R.: The design and construction of deadlock-free concurrent systems. Ph.D. thesis, University of Buckingham (1996)"},{"key":"15_CR22","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). doi:10.1007\/3-540-63533-5_22"},{"issue":"4","key":"15_CR23","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T Murata","year":"1989","unstructured":"Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541\u2013580 (1989)","journal-title":"Proc. IEEE"},{"key":"15_CR24","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, 937\u20131004 (2016)","journal-title":"Formal Aspects Comput."},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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 1020 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). doi:10.1007\/3-540-60630-0_7"},{"key":"15_CR26","doi-asserted-by":"publisher","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)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54580-5_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,21]],"date-time":"2021-04-21T02:51:15Z","timestamp":1618973475000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54580-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662545799","9783662545805"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54580-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]]},"assertion":[{"value":"31 March 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}