{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,8,2]],"date-time":"2022-08-02T10:43:24Z","timestamp":1659437004027},"reference-count":55,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2022,4,7]],"date-time":"2022-04-07T00:00:00Z","timestamp":1649289600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,4,7]],"date-time":"2022-04-07T00:00:00Z","timestamp":1649289600000},"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":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2022,8]]},"DOI":"10.1007\/s10009-022-00650-6","type":"journal-article","created":{"date-parts":[[2022,4,7]],"date-time":"2022-04-07T15:07:13Z","timestamp":1649344033000},"page":"613-633","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Approximate verification of concurrent systems using token structures and invariants"],"prefix":"10.1007","volume":"24","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":[[2022,4,7]]},"reference":[{"key":"650_CR1","doi-asserted-by":"crossref","unstructured":"Agerwala, T., Choed-Amphai, Y.C.: A synthesis rule for concurrent systems. In: Design Automation, 1978. 15th Conference on, pp. 305\u2013311. IEEE (1978)","DOI":"10.1109\/DAC.1978.1585190"},{"issue":"1","key":"650_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/356901.356903","volume":"15","author":"GR Andrews","year":"1983","unstructured":"Andrews, G.R., Schneider, F.B.: Concepts and notations for concurrent programming. ACM Comput. Surv. 15(1), 3\u201343 (1983)","journal-title":"ACM Comput. Surv."},{"key":"650_CR3","unstructured":"Antonino, P.: Verifying concurrent systems by approximations. DPhil thesis, University of Oxford (2018). https:\/\/ora.ox.ac.uk\/objects\/uuid:f75c782c-a168-49b3-bfed-e2715f027157"},{"key":"650_CR4","doi-asserted-by":"crossref","unstructured":"Antonino, P., Gibson-Robinson, T., Roscoe, A.: Efficient deadlock-freedom checking using local analysis and SAT solving. In: IFM, no. 9681 in LNCS, pp. 345\u2013360. Springer (2016)","DOI":"10.1007\/978-3-319-33693-0_22"},{"key":"650_CR5","doi-asserted-by":"crossref","unstructured":"Antonino, P., Gibson-Robinson, T., Roscoe, A.: Tighter reachability criteria for deadlock freedom analysis. In: FM, no. 9995 in LNCS. Springer (2016)","DOI":"10.1007\/978-3-319-48989-6_3"},{"key":"650_CR6","unstructured":"Antonino, P., Gibson-Robinson, T., Roscoe, A.: Experiment package (2018). www.cs.ox.ac.uk\/people\/pedro.antonino\/thepkg.zip"},{"key":"650_CR7","doi-asserted-by":"crossref","unstructured":"Antonino, P., Gibson-Robinson, T., Roscoe, A.W.: The automatic detection of token structures and invariants using SAT checking. In: TACAS, no. 10206 in LNCS, pp. 249\u2013265. Springer (2017)","DOI":"10.1007\/978-3-662-54580-5_15"},{"key":"650_CR8","doi-asserted-by":"crossref","unstructured":"Antonino, P., Gibson-Robinson, T., Roscoe, A.W.: Checking static properties using conservative SAT approximations for reachability. LNCS (2017)","DOI":"10.1007\/978-3-319-70848-5_15"},{"issue":"3","key":"650_CR9","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/s00165-019-00483-2","volume":"31","author":"P Antonino","year":"2019","unstructured":"Antonino, P., Gibson-Robinson, T., Roscoe, A.W.: Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving. Formal Asp. Comput. 31(3), 375\u2013409 (2019)","journal-title":"Formal Asp. Comput."},{"issue":"3","key":"650_CR10","doi-asserted-by":"publisher","first-page":"18:1","DOI":"10.1145\/3335149","volume":"28","author":"P Antonino","year":"2019","unstructured":"Antonino, P., Gibson-Robinson, T., Rosco, A..W.: Efficient verification of concurrent systems using synchronisation analysis and SAT\/SMT solving. ACM Trans. Softw. Eng. Methodol. 28(3), 18:1-18:43 (2019)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"650_CR11","first-page":"31","volume":"8430","author":"P Antonino","year":"2014","unstructured":"Antonino, P., Oliveira, M.M., Sampaio, A., Kristensen, K., Bryans, J.: Leadership election: an industrial SoS application of compositional deadlock verification. NFM, LNCS 8430, 31\u201345 (2014)","journal-title":"NFM, LNCS"},{"key":"650_CR12","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-319-06410-9_5","volume":"8442","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. FM, LNCS 8442, 62\u201377 (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_5","journal-title":"FM, LNCS"},{"issue":"3","key":"650_CR13","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1145\/357103.357110","volume":"2","author":"KR Apt","year":"1980","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)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"650_CR14","doi-asserted-by":"crossref","unstructured":"Attie, P.C., Bensalem, S., Bozga, M., Jaber, M., Sifakis, J., Zaraket, F.A.: An abstract framework for deadlock prevention in BIP. In: FORTE, no. 7892 in LNCS, pp. 161\u2013177. Springer (2013)","DOI":"10.1007\/978-3-642-38592-6_12"},{"issue":"3","key":"650_CR15","doi-asserted-by":"publisher","first-page":"9:1","DOI":"10.1145\/3152910","volume":"26","author":"PC Attie","year":"2018","unstructured":"Attie, P.C., Bensalem, S., Bozga, M., Jaber, M., Sifakis, J., Zaraket, F.A.: Global and local deadlock freedom in BIP. ACM Trans. Softw. Eng. Methodol. 26(3), 9:1-9:48 (2018). https:\/\/doi.org\/10.1145\/3152910","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"650_CR16","doi-asserted-by":"crossref","unstructured":"Attie, P.C., Chockler, H.: Efficiently verifiable conditions for deadlock-freedom of large concurrent programs. In: VMCAI, pp. 465\u2013481. Springer (2005)","DOI":"10.1007\/978-3-540-30579-8_30"},{"key":"650_CR17","unstructured":"Audemard, G., Simon, L.: Predicting Learnt Clauses Quality in Modern SAT Solvers. IJCAI\u201909, pp. 399\u2013404. San Francisco, CA, USA (2009)"},{"key":"650_CR18","volume-title":"Principles of Model Checking (Representation and Mind Series)","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking (Representation and Mind Series). The MIT Press, United States (2008)"},{"key":"650_CR19","doi-asserted-by":"crossref","unstructured":"Batcher, K.E.: Sorting networks and their applications. In: Proceedings of the April 30\u2013May 2, 1968, Spring Joint Computer Conference, AFIPS \u201968 (Spring), pp. 307\u2013314. ACM, New York, NY, USA (1968). 10.1145\/1468075.1468121","DOI":"10.1145\/1468075.1468121"},{"issue":"2","key":"650_CR20","doi-asserted-by":"publisher","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., Sifakis, J., Yan, R.: Component-based verification using incremental design and invariants. Softw. Syst. Model. 15(2), 427\u2013451 (2016). https:\/\/doi.org\/10.1007\/s10270-014-0410-8","journal-title":"Softw. Syst. Model."},{"key":"650_CR21","doi-asserted-by":"crossref","unstructured":"Bensalem, S., Griesmayer, A., Legay, A., Nguyen, T.H., Sifakis, J., Yan, R.: D-finder 2: Towards efficient correctness of incremental design. In: NFM, pp. 453\u2013458 (2011)","DOI":"10.1007\/978-3-642-20398-5_32"},{"issue":"1","key":"650_CR22","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). https:\/\/doi.org\/10.1023\/A:1008744030390","journal-title":"Form. Methods Syst. Des."},{"key":"650_CR23","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without bdds. Tools and Algorithms for the Construction and Analysis of Systems pp. 193\u2013207 (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"key":"650_CR24","doi-asserted-by":"publisher","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":"650_CR25","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Inform. comput. 98(2), 142\u2013170 (1992)","journal-title":"Inform. comput."},{"issue":"4","key":"650_CR26","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/s00165-005-0071-z","volume":"17","author":"S Chaki","year":"2005","unstructured":"Chaki, S., Clarke, E., Ouaknine, J., Sharygina, N., Sinha, N.: Concurrent software verification with states, events, and deadlocks. Form. Asp. Comput. 17(4), 461\u2013483 (2005)","journal-title":"Form. Asp. Comput."},{"key":"650_CR27","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Computer aided verification, pp. 154\u2013169. Springer (2000)","DOI":"10.1007\/10722167_15"},{"issue":"5","key":"650_CR28","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1145\/363095.363143","volume":"11","author":"EW Dijkstra","year":"1968","unstructured":"Dijkstra, E.W.: The structure of the“the”-multiprogramming system. Commun. ACM 11(5), 341\u2013346 (1968)","journal-title":"Commun. ACM"},{"issue":"1\u20134","key":"650_CR29","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":"650_CR30","doi-asserted-by":"crossref","unstructured":"Filho, M.S.C., Oliveira, M.V.M., Sampaio, A., Cavalcanti, A.: Local livelock analysis of component-based models. In: ICFEM, pp. 279\u2013295 (2016)","DOI":"10.1007\/978-3-319-47846-3_18"},{"key":"650_CR31","first-page":"187","volume":"8413","author":"T Gibson-Robinson","year":"2014","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.: FDR3 \u2013 A Modern Refinement Checker for CSP. TACAS, LNCS 8413, 187\u2013201 (2014)","journal-title":"TACAS, LNCS"},{"key":"650_CR32","first-page":"188","volume":"9058","author":"T Gibson-Robinson","year":"2015","unstructured":"Gibson-Robinson, T., Hansen, H., Roscoe, A., Wang, X.: Practical partial order reduction for CSP. NFM, LNCS 9058, 188\u2013203 (2015)","journal-title":"NFM, LNCS"},{"issue":"2","key":"650_CR33","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"},{"issue":"14\u201315","key":"650_CR34","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1016\/j.ipl.2010.04.021","volume":"110","author":"S Gruner","year":"2010","unstructured":"Gruner, S., Steyn, T.J.: Deadlock-freeness of hexagonal systolic arrays. Inf. Process. Lett. 110(14\u201315), 539\u2013543 (2010). https:\/\/doi.org\/10.1016\/j.ipl.2010.04.021","journal-title":"Inf. Process. Lett."},{"key":"650_CR35","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, United States (1985)"},{"key":"650_CR36","doi-asserted-by":"crossref","unstructured":"Lambertz, C., Majster-Cederbaum, M.: Analyzing Component-Based Systems on the Basis of Architectural Constraints. In: FSEN, pp. 64\u201379. Springer (2011)","DOI":"10.1007\/978-3-642-29320-7_5"},{"key":"650_CR37","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":"650_CR38","doi-asserted-by":"crossref","unstructured":"Martin, J., Jassim, S.: An efficient technique for deadlock analysis of large scale process networks. In: FME \u201997, pp. 418\u2013441 (1997)","DOI":"10.1007\/3-540-63533-5_22"},{"key":"650_CR39","unstructured":"Martin, J.M.R.: The design and construction of deadlock-free concurrent systems. Ph.D. thesis, University of Buckingham (1996)"},{"key":"650_CR40","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient smt solver. In: TACAS, pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"650_CR41","doi-asserted-by":"publisher","unstructured":"Murata, T.: Petri nets: Properties, analysis and applications. Proceedings of the IEEE 77(4), 541\u2013580 (1989). https:\/\/doi.org\/10.1109\/5.24143","DOI":"10.1109\/5.24143"},{"key":"650_CR42","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-016-0375-1","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. Form. Asp. Comput. (2016). https:\/\/doi.org\/10.1007\/s00165-016-0375-1","journal-title":"Form. Asp. Comput."},{"key":"650_CR43","doi-asserted-by":"crossref","unstructured":"Otoni, R., Cavalcanti, A., Sampaio, A.: Local analysis of determinism for CSP. In: Formal Methods: Foundations and Applications - 20th Brazilian Symposium, SBMF 2017, Recife, Brazil, November 29 - December 1, 2017, Proceedings, pp. 107\u2013124 (2017)","DOI":"10.1007\/978-3-319-70848-5_8"},{"key":"650_CR44","doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Palikareva, H., Roscoe, A.W., Worrell, J.: A static analysis framework for livelock freedom in CSP. LMCS 9(3) (2013)","DOI":"10.2168\/LMCS-9(3:24)2013"},{"issue":"10","key":"650_CR45","doi-asserted-by":"publisher","first-page":"1178","DOI":"10.1016\/j.scico.2011.07.008","volume":"77","author":"H Palikareva","year":"2012","unstructured":"Palikareva, H., Ouaknine, J., Roscoe, A.: SAT-solving in CSP trace refinement. Sci. Comput. Program. 77(10), 1178\u20131197 (2012)","journal-title":"Sci. Comput. Program."},{"key":"650_CR46","doi-asserted-by":"crossref","unstructured":"Peled, D.: All from one, one for all: on model checking using representatives. In: Computer Aided Verification, pp. 409\u2013423. Springer (1993)","DOI":"10.1007\/3-540-56922-7_34"},{"issue":"3","key":"650_CR47","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1145\/356698.356702","volume":"9","author":"JL Peterson","year":"1977","unstructured":"Peterson, J.L.: Petri nets. ACM Comput. Surv. 9(3), 223\u2013252 (1977)","journal-title":"ACM Comput. Surv."},{"key":"650_CR48","unstructured":"Plotkin, G.: A structural approach to operational semantics. Tech. rep., DAIMI FN-19, Computer Science Dept, Aarhus University (1981)"},{"key":"650_CR49","unstructured":"Ramos, R.T.: Systematic development of trustworthy component-based systems. Ph.D. thesis, Universidade Federal de Pernambuco (2011)"},{"key":"650_CR50","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-258-0","volume-title":"Understanding Concurrent Systems","author":"A Roscoe","year":"2010","unstructured":"Roscoe, A.: Understanding Concurrent Systems. Springer, Berlin (2010)"},{"key":"650_CR51","unstructured":"Roscoe, A.W.: The theory and practice of concurrency. Prentice Hall, United States (1998)"},{"issue":"3","key":"650_CR52","doi-asserted-by":"publisher","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":"650_CR53","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^{{20}}$$ dining philosophers for deadlock. In: TACAS, pp. 133\u2013152 (1995)","DOI":"10.1007\/3-540-60630-0_7"},{"issue":"4","key":"650_CR54","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00709154","volume":"1","author":"A Valmari","year":"1992","unstructured":"Valmari, A.: A stubborn attack on state explosion. Form. Methods Syst. Des. 1(4), 297\u2013322 (1992)","journal-title":"Form. Methods Syst. Des."},{"key":"650_CR55","doi-asserted-by":"crossref","unstructured":"Yeh, W.J., Young, M.: Compositional reachability analysis using process algebra. In: Proceedings of the symposium on Testing, analysis, and verification, pp. 49\u201359. ACM (1991)","DOI":"10.1145\/120807.120812"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00650-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-022-00650-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00650-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,2]],"date-time":"2022-08-02T10:06:47Z","timestamp":1659434807000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-022-00650-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,7]]},"references-count":55,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,8]]}},"alternative-id":["650"],"URL":"https:\/\/doi.org\/10.1007\/s10009-022-00650-6","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,7]]},"assertion":[{"value":"7 April 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}