{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:38:13Z","timestamp":1740109093897,"version":"3.37.3"},"reference-count":62,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T00:00:00Z","timestamp":1559347200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T00:00:00Z","timestamp":1557705600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2019,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>This work develops a type of local analysis that can prove concurrent systems deadlock free. As opposed to examining the overall behaviour of a system, local analysis consists of examining the behaviour of small parts of the system to yield a given property. We analyse pairs of interacting components to approximate system reachability and propose a new sound but incomplete\/approximate framework that checks deadlock and local-deadlock freedom. By replacing exact reachability by this approximation, it looks for deadlock (or local-deadlock) candidates, namely, blocked (locally-blocked) system states that lie within our approximation. This characterisation improves on the precision of current approximate techniques. In particular, it can tackle non-hereditary deadlock-free systems, namely, deadlock-free systems that have a deadlocking subsystem. These are neglected by most approximate techniques. Furthermore, we demonstrate how SAT checkers can be used to efficiently implement our framework, which, typically, scales better than current techniques for deadlock-freedom analysis. This is demonstrated by a series of practical experiments.<\/jats:p>","DOI":"10.1007\/s00165-019-00483-2","type":"journal-article","created":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T02:10:39Z","timestamp":1557799839000},"page":"375-409","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving"],"prefix":"10.1145","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5627-0910","authenticated-orcid":false,"given":"Pedro","family":"Antonino","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Gibson-Robinson","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A. W.","family":"Roscoe","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Attie PC Bensalem S Bozga M Jaber M Sifakis J Zaraket FA (2013) An abstract framework for deadlock prevention in BIP. In:  FORTE number 7892 in LNCS. Springer pp 161\u2013177","DOI":"10.1007\/978-3-642-38592-6_12"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Attie PC Bensalem S Bozga M Jaber M Sifakis J Zaraket FA (2018) Global and local deadlock freedom in BIP.  ACM Trans Softw Eng Methodol 26(3):9:1\u20139:48","DOI":"10.1145\/3152910"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.106975"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Attie PC Chockler H (2005) Efficiently verifiable conditions for deadlock-freedom of large concurrent programs. In: VMCAI. Springer pp 465\u2013481","DOI":"10.1007\/978-3-540-30579-8_30"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/357103.357110"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Antonino P Gibson-Robinson T Roscoe AW (2016) Efficient deadlock-freedom checking using local analysis and SAT solving. In: IFM number 9681 in LNCS. Springer pp 345\u2013360","DOI":"10.1007\/978-3-319-33693-0_22"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Antonino P Gibson-Robinson T Roscoe AW (2016) Tighter reachability criteria for deadlock freedom analysis. In:  FM number 9995 in LNCS. Springer","DOI":"10.1007\/978-3-319-48989-6_3"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Antonino P Gibson-Robinson T Roscoe AW (2017) The automatic detection of token structures and invariants using SAT checking. In:  TACAS number 10206 in LNCS. Springer pp 249\u2013265","DOI":"10.1007\/978-3-662-54580-5_15"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Antonino P Gibson-Robinson T Roscoe AW (2017) Checking static properties using conservative sat approximations for reachability. In:  Formal methods: foundations and applications. Springer pp 233\u2013250","DOI":"10.1007\/978-3-319-70848-5_15"},{"key":"e_1_2_1_2_10_2","unstructured":"Antonino P Gibson-Robinson T Roscoe AW (2018) Experiment package. www.cs.ox.ac.uk\/people\/pedro.antonino\/facpkg.zip"},{"key":"e_1_2_1_2_11_2","unstructured":"Antonino P (2018) Verifying concurrent systems by approximations. DPhil thesis University of Oxford. https:\/\/ora.ox.ac.uk\/objects\/uuid:f75c782c-a168-49b3-bfed-e2715f027157"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Antonino P Oliveira MM Sampaio A Kristensen K Bryans J (2014) Leadership election: an industrial SoS application of compositional deadlock verification. In: NFM volume 8430 of LNCS pp 31\u201345","DOI":"10.1007\/978-3-319-06200-6_3"},{"key":"e_1_2_1_2_13_2","first-page":"399","volume-title":"IJCAI'09","author":"Audemard G","year":"2009"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Antonino P Sampaio A Woodcock J (2014) A refinement based strategy for local deadlock analysis of networks of CSP processes. In:  FM volume 8442 of  LNCS pp 62\u201377","DOI":"10.1007\/978-3-319-06410-9_5"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-014-0410-8"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Biere A Cimatti A Clarke E Zhu Y (1999) Symbolic model checking without bdds. In:  Tools and algorithms for the construction and analysis of systems pp 193\u2013207","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Bensalem S Griesmayer A Legay A Nguyen T-H Sifakis J Yan R (2011) D-finder 2: towards efficient correctness of incremental design. In:  NFM pp 453\u2013458","DOI":"10.1007\/978-3-642-20398-5_32"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/116873.116875"},{"key":"e_1_2_1_2_20_2","unstructured":"Baier C Katoen J-P (2008)  Principles of model checking (representation and mind series). The MIT Press"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008744030390"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01784721"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01384316"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-005-0071-z"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/356586.356588"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Clarke E Grumberg O Jha S Lu Y Veith H (2000) Counterexample-guided abstraction refinement. In:  Computer aided verification. Springer pp 154\u2013169","DOI":"10.1007\/10722167_15"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.310668"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.489078"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/1040291.1040292"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Conserva Filho MS Oliveira MVM Sampaio A Cavalcanti A (2016) Local livelock analysis of component-based models. In:  ICFEM pp 279\u2013295","DOI":"10.1007\/978-3-319-47846-3_18"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson T Armstrong P Boulgakov A Roscoe AW (2014) FDR3\u2014a modern refinement checker for CSP. In:  TACAS volume 8413 of  LNCS pp 187\u2013201","DOI":"10.1007\/978-3-642-54862-8_13"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson T Hansen H Roscoe AW Wang Xu (2015) Practical partial order reduction for CSP. In:  NFM volume 9058 of  LNCS. Springer pp 188\u2013203","DOI":"10.1007\/978-3-319-17524-9_14"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01383879"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.5555\/3921"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.5555\/1734069"},{"key":"e_1_2_1_2_36_2","unstructured":"Jezequel L Lime D (2016) Lazy reachability analysis in distributed systems. In: Desharnais J Jagadeesan R (eds)  CONCUR 2016 volume\u00a059 of  Leibniz international proceedings in informatics (LIPIcs). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik Dagstuhl Germany 2016 pp 17:1\u201317:14"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90025-D"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229904"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Lambertz C Majster-Cederbaum M (2011) Analyzing component-based systems on the basis of architectural constraints. In:  FSEN. Springer pp 64\u201379","DOI":"10.1007\/978-3-642-29320-7_5"},{"key":"e_1_2_1_2_40_2","unstructured":"Martin Jeremy MR (1996)  The design and construction of deadlock-free concurrent systems. Ph.D. thesis University of Buckingham"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Martin JMR Jassim SA (1997) An efficient technique for deadlock analysis of large scale process networks. In:  FME '97 pp 418\u2013441","DOI":"10.1007\/3-540-63533-5_22"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Oliveira MVM Antonino P Ramos R Sampaio A Mota A Roscoe AW (2016) Rigorous development of component-based systems using component metadata and patterns.  Form Asp Comput 1\u201368","DOI":"10.1007\/s00165-016-0375-1"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Otoni R Cavalcanti A Sampaio A (2017) Local analysis of determinism for CSP. In:  Proceedings of formal methods: foundations and applications\u201420th Brazilian symposium SBMF 2017 Recife Brazil 29 November\u20131 December 2017 pp 107\u2013124","DOI":"10.1007\/978-3-319-70848-5_8"},{"key":"e_1_2_1_2_44_2","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"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Peled D (1993) All from one one for all: on model checking using representatives. In:  Computer aided verification. Springer pp 409\u2013423","DOI":"10.1007\/3-540-56922-7_34"},{"key":"e_1_2_1_2_46_2","unstructured":"Plotkin GD (1981) A structural approach to operational semantics. Technical report DAIMI FN-19 Computer Science Department Aarhus University"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2011.07.008"},{"key":"e_1_2_1_2_48_2","unstructured":"Ramos RT (2011)  Systematic development of trustworthy component-based systems. Ph.D. thesis Universidade Federal de Pernambuco"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/58564.59295"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(87)90004-6"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"crossref","unstructured":"Roscoe AW Gardiner PHB Goldsmith M Hulance JR Jackson DM Scattergood JB (1995) Hierarchical compression for model-checking CSP or how to check 1020 dining philosophers for deadlock. In:  TACAS pp 133\u2013152","DOI":"10.1007\/3-540-60630-0_7"},{"volume-title":"The theory and practice of concurrency","year":"1998","author":"Roscoe AW","key":"e_1_2_1_2_52_2"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"crossref","unstructured":"Roscoe A.W.: Understanding Concurrent Systems. Springer (2010)","DOI":"10.1007\/978-1-84882-258-0"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(70)80006-X"},{"key":"e_1_2_1_2_55_2","first-page":"334","volume-title":"A class of simple communication patterns","author":"Scholten CS","year":"1982"},{"key":"e_1_2_1_2_56_2","unstructured":"Tarry G (1895) Le probleme des labyrinthes.  Nouvelles annales de math\u00e9matiques. journal des candidats aux \u00e9coles polytechnique et normale 14:187\u2013190"},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139168724"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68972-2_16"},{"key":"e_1_2_1_2_59_2","unstructured":"Tseitin G (1968) On the complexity of derivation in propositional calculus.  Stud Constrained Math Math Logic"},{"key":"e_1_2_1_2_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00709154"},{"key":"e_1_2_1_2_61_2","doi-asserted-by":"publisher","DOI":"10.1049\/ip-e.1989.0025"},{"key":"e_1_2_1_2_62_2","doi-asserted-by":"crossref","unstructured":"Yeh WJ Young M (1991) Compositional reachability analysis using process algebra. In:  Proceedings of the symposium on testing analysis and verification. ACM pp 49\u201359","DOI":"10.1145\/120807.120812"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-019-00483-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-019-00483-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-019-00483-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-019-00483-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,7]],"date-time":"2022-01-07T06:55:52Z","timestamp":1641538552000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-019-00483-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6]]},"references-count":62,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,6]]}},"alternative-id":["10.1007\/s00165-019-00483-2"],"URL":"https:\/\/doi.org\/10.1007\/s00165-019-00483-2","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2019,6]]},"assertion":[{"value":"19 July 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 April 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 May 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}