{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:28:31Z","timestamp":1750220911632,"version":"3.41.0"},"reference-count":85,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2019,7,18]],"date-time":"2019-07-18T00:00:00Z","timestamp":1563408000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Innovate UK and the Aerospace Technology Institute","award":["113099"],"award-info":[{"award-number":["113099"]}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/N022777"],"award-info":[{"award-number":["EP\/N022777"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002322","name":"Coordena\u00e7\u00e3o de Aperfei\u00e7oamento de Pessoal de N\u00edvel Superior","doi-asserted-by":"crossref","award":["Process no: 13201\/13-1"],"award-info":[{"award-number":["Process no: 13201\/13-1"]}],"id":[{"id":"10.13039\/501100002322","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2019,7,31]]},"abstract":"<jats:p>\n            This article investigates how the use of approximations can make the formal verification of concurrent systems scalable. We propose the idea of\n            <jats:italic>synchronisation analysis<\/jats:italic>\n            to automatically capture global invariants and approximate reachability. We calculate invariants on how components participate on global system synchronisations and use a notion of consistency between these invariants to establish whether components can effectively communicate to reach some system state. Our synchronisation-analysis techniques try to show either that a system state is unreachable by demonstrating that components cannot agree on the order they participate in system rules or that a system state is unreachable by demonstrating components cannot agree on the number of times they participate on system rules. These fully automatic techniques are applied to check deadlock and local-deadlock freedom in the\n            <jats:italic>PairStatic<\/jats:italic>\n            framework. It extends\n            <jats:italic>Pair<\/jats:italic>\n            (a recent framework where we use pure pairwise analysis of components and SAT checkers to check deadlock and local-deadlock freedom) with techniques to carry out synchronisation analysis. So, not only can it compute the same local invariants that\n            <jats:italic>Pair<\/jats:italic>\n            does, it can leverage\n            <jats:italic>global<\/jats:italic>\n            invariants found by synchronisation analysis, thereby improving the reachability approximation and tightening our verifications. We implement\n            <jats:italic>PairStatic<\/jats:italic>\n            in our DeadlOx tool using SAT\/SMT and demonstrate the improvements they create in checking (local) deadlock freedom.\n          <\/jats:p>","DOI":"10.1145\/3335149","type":"journal-article","created":{"date-parts":[[2019,7,19]],"date-time":"2019-07-19T13:17:14Z","timestamp":1563542234000},"page":"1-43","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Efficient Verification of Concurrent Systems Using Synchronisation Analysis and SAT\/SMT Solving"],"prefix":"10.1145","volume":"28","author":[{"given":"Pedro","family":"Antonino","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Oxford, Oxford, Oxfordshire, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Gibson-Robinson","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, Oxford, Oxfordshire, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A. W.","family":"Roscoe","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, Oxford, Oxfordshire, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,7,18]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Pedro Antonino. 2018. Verifying Concurrent Systems by Approximations. Ph.D. Thesis. University of Oxford Oxford UK. Retrieved from: https:\/\/ora.ox.ac.uk\/objects\/uuid:f75c782c-a168-49b3-bfed-e2715f027157.  Pedro Antonino. 2018. Verifying Concurrent Systems by Approximations. Ph.D. Thesis. University of Oxford Oxford UK. Retrieved from: https:\/\/ora.ox.ac.uk\/objects\/uuid:f75c782c-a168-49b3-bfed-e2715f027157."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33693-0_22"},{"volume-title":"Proceedings of the FM (LNCS). Springer.","author":"Antonino Pedro","key":"e_1_2_1_3_1"},{"key":"e_1_2_1_4_1","unstructured":"Pedro Antonino Thomas Gibson-Robinson and A. W. Roscoe. 2018. Experiment package. Retrieved from: www.cs.ox.ac.uk\/people\/pedro.antonino\/tosempkg.zip.  Pedro Antonino Thomas Gibson-Robinson and A. W. Roscoe. 2018. Experiment package. Retrieved from: www.cs.ox.ac.uk\/people\/pedro.antonino\/tosempkg.zip."},{"volume-title":"Proceedings of the SBMF. 233--250","author":"Antonino Pedro","key":"e_1_2_1_5_1"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00483-2"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06200-6_3"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_5"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/357103.357110"},{"volume":"7892","volume-title":"Proceedings of the FORTE (LNCS).","author":"Attie Paul C.","key":"e_1_2_1_10_1"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3152910"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_30"},{"volume-title":"Proceedings of the IJCAI. 399--404","year":"2009","author":"Audemard Gilles","key":"e_1_2_1_13_1"},{"key":"e_1_2_1_14_1","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking (Representation and Mind Series). The MIT Press Cambridge MA.   Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking (Representation and Mind Series). The MIT Press Cambridge MA."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2011.27"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2006.27"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1090\/qam\/102435"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-014-0410-8"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1986308.1986344"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008744030390"},{"volume-title":"Proceedings of the CAV","author":"Beyer Dirk","key":"e_1_2_1_21_1"},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Armin Biere Alessandro Cimatti Edmund Clarke and Yunshan Zhu. 1999. Symbolic model checking without BDDs. Tools and Algorithms for the Construction and Analysis of Systems (1999) 193--207.   Armin Biere Alessandro Cimatti Edmund Clarke and Yunshan Zhu. 1999. Symbolic model checking without BDDs. Tools and Algorithms for the Construction and Analysis of Systems (1999) 193--207.","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1118537.1123063"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01784721"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Gerardo Canfora and Massimiliano Di Penta. 2006. Service-oriented architectures testing: A survey. Softw. Eng. Springer 78--105.  Gerardo Canfora and Massimiliano Di Penta. 2006. Service-oriented architectures testing: A survey. Softw. Eng. Springer 78--105.","DOI":"10.1007\/978-3-540-95888-8_4"},{"volume-title":"Formal Methods: Foundations and Applications, Simone Cavalheiro and Jos\u00e9 Fiadeiro (Eds.)","author":"Cavalcanti Ana","key":"e_1_2_1_28_1"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-005-0071-z"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.310668"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734089"},{"key":"e_1_2_1_32_1","unstructured":"Edmund M. Clarke Orna Grumberg and Doron Peled. 1999. Model Checking. The MIT Press Cambridge MA.   Edmund M. Clarke Orna Grumberg and Doron Peled. 1999. Model Checking. The MIT Press Cambridge MA."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/242223.242257"},{"volume-title":"Proceedings of the SoSE. 451--456","author":"Coleman J. W.","key":"e_1_2_1_34_1"},{"key":"e_1_2_1_35_1","unstructured":"Thomas H. Cormen Charles E. Leiserson Ronald L. Rivest and Clifford Stein. 2009. Introduction to Algorithms Third Edition. The MIT Press Cambridge MA.   Thomas H. Cormen Charles E. Leiserson Ronald L. Rivest and Clifford Stein. 2009. Introduction to Algorithms Third Edition. The MIT Press Cambridge MA."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"volume-title":"Proceedings of the ASE. 267--270","author":"Csertan G.","key":"e_1_2_1_38_1"},{"key":"e_1_2_1_39_1","unstructured":"Naiem Dathi. 1989. Deadlock and Deadlock Freedom. Ph.D. Thesis. University of Oxford Oxford UK.   Naiem Dathi. 1989. Deadlock and Deadlock Freedom. Ph.D. Thesis. University of Oxford Oxford UK."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/503271.503226"},{"key":"e_1_2_1_41_1","doi-asserted-by":"crossref","unstructured":"Luca de Alfaro and Thomas A. Henzinger. 2001. Interface theories for component-based design. In Embedded Software (LNCS) Thomas A. Henzinger and Christoph M. Kirsch (Eds.). Springer Berlin 148--165.   Luca de Alfaro and Thomas A. Henzinger. 2001. Interface theories for component-based design. In Embedded Software (LNCS) Thomas A. Henzinger and Christoph M. Kirsch (Eds.). Springer Berlin 148--165.","DOI":"10.1007\/3-540-45449-7_11"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2008.923410"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040291.1040292"},{"volume-title":"Proceedings of the ICFEM. 279--295","year":"2016","author":"Conserva Filho Madiel S.","key":"e_1_2_1_45_1"},{"volume-title":"Collaborative Networks in the Internet of Services, Luis M. Camarinha-Matos","author":"Fitzgerald John","key":"e_1_2_1_46_1"},{"key":"e_1_2_1_47_1","unstructured":"D. R. Ford and D. R. Fulkerson. 2010. Flows in Networks. Princeton University Press Princeton NJ.   D. R. Ford and D. R. Fulkerson. 2010. Flows in Networks. Princeton University Press Princeton NJ."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOSE.2007.14"},{"key":"e_1_2_1_49_1","first-page":"187","article-title":"FDR3\u2014a modern refinement checker for CSP","volume":"8413","author":"Gibson-Robinson Thomas","year":"2014","journal-title":"Proceedings of the TACAS (LNCS)"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-17524-9_14"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01383879"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2010.04.021"},{"key":"e_1_2_1_53_1","unstructured":"C. A. R. Hoare. 1985. Communicating Sequential Processes. Prentice Hall Upper Saddle River NJ.   C. A. R. Hoare. 1985. Communicating Sequential Processes. Prentice Hall Upper Saddle River NJ."},{"key":"e_1_2_1_54_1","volume-title":"Decision Procedures: An Algorithmic Point of View","author":"Kroening Daniel","year":"2008","edition":"1"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29320-7_5"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229904"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001659970003"},{"volume-title":"Proceedings of the ASE. 255--258","author":"Lilius J.","key":"e_1_2_1_58_1"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-015-0492-y"},{"key":"e_1_2_1_60_1","unstructured":"Nancy A. Lynch and Mark R. Tuttle. 1988. An introduction to input\/output automata. (1988).  Nancy A. Lynch and Mark R. Tuttle. 1988. An introduction to input\/output automata. (1988)."},{"volume-title":"Proceedings of the FME. 418--441","author":"Martin J. M. R.","key":"e_1_2_1_61_1"},{"key":"e_1_2_1_62_1","unstructured":"Jeremy M. R. Martin. 1996. The Design and Construction of Deadlock-Free Concurrent Systems. Ph.D. Dissertation. University of Buckingham Buckingham UK.  Jeremy M. R. Martin. 1996. The Design and Construction of Deadlock-Free Concurrent Systems. Ph.D. Dissertation. University of Buckingham Buckingham UK."},{"key":"e_1_2_1_63_1","unstructured":"Robin Milner. 1989. Communication and Concurrency. Prentice Hall Upper Saddle River NJ.   Robin Milner. 1989. Communication and Concurrency. Prentice Hall Upper Saddle River NJ."},{"volume-title":"Proceedings of the IROS. 3869--3876","author":"Miyazawa A.","key":"e_1_2_1_64_1"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.24143"},{"key":"e_1_2_1_66_1","doi-asserted-by":"crossref","unstructured":"Flemming Nielson Hanne R. Nielson and Chris Hankin. 1999. Principles of Program Analysis. Springer-Verlag New York Inc.   Flemming Nielson Hanne R. Nielson and Chris Hankin. 1999. Principles of Program Analysis. Springer-Verlag New York Inc.","DOI":"10.1007\/978-3-662-03811-6"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-016-0375-1"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70848-5_8"},{"key":"e_1_2_1_69_1","doi-asserted-by":"crossref","unstructured":"Jo\u00ebl Ouaknine Hristina Palikareva A. W. Roscoe and James Worrell. 2013. A static analysis framework for livelock freedom in CSP. Logic. Meth. Comput. Sci. 9 3 (2013).  Jo\u00ebl Ouaknine Hristina Palikareva A. W. Roscoe and James Worrell. 2013. A static analysis framework for livelock freedom in CSP. Logic. Meth. Comput. Sci. 9 3 (2013).","DOI":"10.2168\/LMCS-9(3:24)2013"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1137\/0216062"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2011.07.008"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.5555\/647762.735490"},{"key":"e_1_2_1_74_1","unstructured":"Rodrigo Teixeira Ramos. 2011. Systematic Development of Trustworthy Component-based Systems. Ph.D. Dissertation. Universidade Federal de Pernambuco Recife Brazil.  Rodrigo Teixeira Ramos. 2011. Systematic Development of Trustworthy Component-based Systems. Ph.D. Dissertation. Universidade Federal de Pernambuco Recife Brazil."},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01407862"},{"key":"e_1_2_1_76_1","doi-asserted-by":"crossref","unstructured":"A. W. Roscoe. 2010. Understanding Concurrent Systems. Springer.   A. W. Roscoe. 2010. Understanding Concurrent Systems. Springer.","DOI":"10.1007\/978-1-84882-258-0"},{"volume-title":"Programming of Transputer Based Machines: Proceedings of 7th occam User Group Technical Meeting, Muntean et al. (Eds.). IOS B.V.","year":"1987","author":"Roscoe A. W.","key":"e_1_2_1_77_1"},{"key":"e_1_2_1_78_1","unstructured":"A. W. Roscoe. 1998. The Theory and Practice of Concurrency. Prentice Hall Upper Saddle River NJ.   A. W. Roscoe. 1998. The Theory and Practice of Concurrency. Prentice Hall Upper Saddle River NJ."},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(87)90004-6"},{"volume-title":"Proceedings of the TACAS. 133--152","author":"Roscoe A. W.","key":"e_1_2_1_80_1"},{"key":"e_1_2_1_81_1","doi-asserted-by":"crossref","unstructured":"C. S. Scholten and Edsger W. Dijkstra. 1982. A Class of Simple Communication Patterns. Springer New York New York NY 334--337.  C. S. Scholten and Edsger W. Dijkstra. 1982. A Class of Simple Communication Patterns. Springer New York New York NY 334--337.","DOI":"10.1007\/978-1-4612-5695-3_60"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2003.1231146"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00709154"},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592436"},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/120807.120812"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3335149","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3335149","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:45:01Z","timestamp":1750203901000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3335149"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,18]]},"references-count":85,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,7,31]]}},"alternative-id":["10.1145\/3335149"],"URL":"https:\/\/doi.org\/10.1145\/3335149","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"type":"print","value":"1049-331X"},{"type":"electronic","value":"1557-7392"}],"subject":[],"published":{"date-parts":[[2019,7,18]]},"assertion":[{"value":"2018-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-07-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}