{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T08:45:36Z","timestamp":1773996336609,"version":"3.50.1"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2021,2,9]],"date-time":"2021-02-09T00:00:00Z","timestamp":1612828800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"NRF Singapore under National Cyber-security R8D (NCR) programme"},{"name":"NRF Investigatorship Award","award":["NRFI06-2020-0022"],"award-info":[{"award-number":["NRFI06-2020-0022"]}]},{"DOI":"10.13039\/501100022210","name":"National Satellite of Excellence in Trustworthy Software Systems","doi-asserted-by":"crossref","award":["NRF2018NCR-NSOE003"],"award-info":[{"award-number":["NRF2018NCR-NSOE003"]}],"id":[{"id":"10.13039\/501100022210","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Ministry of Education, Singapore, under its Academic Tier-2 Research Fund","award":["MOE2018-T2-1-068"],"award-info":[{"award-number":["MOE2018-T2-1-068"]}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["61872016"],"award-info":[{"award-number":["61872016"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2021,3,31]]},"abstract":"<jats:p>\n            To make feasible and scalable the verification of large and complex concurrent systems, it is necessary the use of compositional techniques even at the highest abstraction layers. When focusing on the lowest software abstraction layers, such as the implementation or the machine code, the high level of detail of those layers makes the direct verification of properties very difficult and expensive. It is therefore essential to use techniques allowing to simplify the verification on these layers. One technique to tackle this challenge is\n            <jats:italic>top-down verification<\/jats:italic>\n            where by means of simulation properties verified on top layers (representing abstract specifications of a system) are propagated down to the lowest layers (that are an implementation of the top layers). There is no need to say that simulation of concurrent systems implies a greater level of complexity, and having compositional techniques to check simulation between layers is also desirable when seeking for both feasibility and scalability of the refinement verification. In this article, we present\n            <jats:bold>CSim<\/jats:bold>\n            <jats:sup>\n              <jats:italic>2<\/jats:italic>\n            <\/jats:sup>\n            a (compositional) rely-guarantee-based framework for the\n            <jats:italic>top-down verification<\/jats:italic>\n            of complex concurrent systems in the Isabelle\/HOL theorem prover.\n            <jats:bold>CSim<\/jats:bold>\n            <jats:sup>\n              <jats:italic>2<\/jats:italic>\n            <\/jats:sup>\n            uses CSimpl, a language with a high degree of expressiveness designed for the specification of concurrent programs. Thanks to its expressibility, CSimpl is able to model many of the features found in real world programming languages like exceptions, assertions, and procedures.\n            <jats:bold>CSim<\/jats:bold>\n            <jats:sup>\n              <jats:italic>2<\/jats:italic>\n            <\/jats:sup>\n            provides a framework for the verification of rely-guarantee properties to compositionally reason on CSimpl specifications. Focusing on top-down verification,\n            <jats:bold>CSim<\/jats:bold>\n            <jats:sup>\n              <jats:italic>2<\/jats:italic>\n            <\/jats:sup>\n            provides a simulation-based framework for the preservation of CSimpl rely-guarantee properties from specifications to implementations. By using the simulation framework, properties proven on the top layers (abstract specifications) are compositionally propagated down to the lowest layers (source or machine code) in each concurrent component of the system. Finally, we show the usability of\n            <jats:bold>CSim<\/jats:bold>\n            <jats:sup>\n              <jats:italic>2<\/jats:italic>\n            <\/jats:sup>\n            by running a case study over two CSimpl specifications of an Arinc-653 communication service. In this case study, we prove a complex property on a specification, and we use\n            <jats:bold>CSim<\/jats:bold>\n            <jats:sup>\n              <jats:italic>2<\/jats:italic>\n            <\/jats:sup>\n            to preserve the property on lower abstraction layers.\n          <\/jats:p>","DOI":"10.1145\/3436808","type":"journal-article","created":{"date-parts":[[2021,2,10]],"date-time":"2021-02-10T13:45:21Z","timestamp":1612964721000},"page":"1-46","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["<b>CSim<\/b>\n            <sup>\n              <i>2<\/i>\n            <\/sup>"],"prefix":"10.1145","volume":"43","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2755-3089","authenticated-orcid":false,"given":"David","family":"Sanan","sequence":"first","affiliation":[{"name":"Nanyang Technological University, Singapore"}]},{"given":"Yongwang","family":"Zhao","sequence":"additional","affiliation":[{"name":"Zhejiang University, Hangzhou, China"}]},{"given":"Shang-Wei","family":"Lin","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore"}]},{"given":"Liu","family":"Yang","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore"}]}],"member":"320","published-online":{"date-parts":[[2021,2,9]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"Aeronautical Radio Inc. 2015. ARINC Specification 653: Avionics Application Software Standard Interface Part 1\u2014Required Services. Aeronautical Radio Inc."},{"key":"e_1_2_2_2_1","volume-title":"Verified Software: Theories","author":"Alkassar Eyad","unstructured":"Eyad Alkassar, Mark A. Hillebrand, Dirk Leinenbach, Norbert W. Schirmer, and Artem Starostin. 2008. The verisoft approach to systems verification. In Verified Software: Theories, Tools, Experiments, Natarajan Shankar and Jim Woodcock (Eds.). Springer, Berlin, 209--224."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_6"},{"key":"e_1_2_2_4_1","volume-title":"CPAchecker: A tool for configurable software verification","author":"Beyer Dirk","unstructured":"Dirk Beyer and M. Erkan Keremoglu. 2011. CPAchecker: A tool for configurable software verification. In Computer Aided Verification, Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer, Berlin, 184--190."},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1993.287596"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11970-5_7"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2668138.2668142"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exm030"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2508859.2516702"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_26"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-016-0384-0"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_22"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-912-1"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_2_17_1","volume-title":"Refinement in the Formal Verification of the seL4 Microkernel","author":"Klein Gerwin","unstructured":"Gerwin Klein, Thomas Sewell, and Simon Winwood. 2010. Refinement in the Formal Verification of the seL4 Microkernel. Springer US, Boston, MA, 323--339."},{"key":"e_1_2_2_18_1","volume-title":"Proceedings of the International Conference on Computer-Aided Design (ICCAD\u201907)","author":"Kundu Sudipta","year":"2007","unstructured":"Sudipta Kundu, Sorin Lerner, and Rajesh Gupta. 2007. Automated refinement checking of concurrent systems. In Proceedings of the International Conference on Computer-Aided Design (ICCAD\u201907). 318--325."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2576235"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_23"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.24"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765712.1765738"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-49020-3_13"},{"key":"e_1_2_2_25_1","volume-title":"Paulson","author":"Nipkow Tobias","year":"2002","unstructured":"Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. 2002. Isabelle\/HOL: A Proof Assistant for Higher-order Logic. Springer-Verlag, Berlin."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_2_2_27_1","doi-asserted-by":"crossref","unstructured":"David San\u00e1n Yongwang Zhao Zhe Hou Fuyuan Zhang Alwen Tiu and Yang Liu. 2017. CSimpl: A rely-guarantee-based framework for verifying concurrent programs. In Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201917) Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS\u201917). 481--498.","DOI":"10.1007\/978-3-662-54577-5_28"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190234"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211617"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-95582-7_31"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_29"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2016.2569414"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_11"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3436808","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3436808","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T17:45:05Z","timestamp":1750268705000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3436808"}},"subtitle":["Compositional Top-down Verification of Concurrent Systems using Rely-Guarantee"],"short-title":[],"issued":{"date-parts":[[2021,2,9]]},"references-count":32,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2021,3,31]]}},"alternative-id":["10.1145\/3436808"],"URL":"https:\/\/doi.org\/10.1145\/3436808","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,2,9]]},"assertion":[{"value":"2019-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-02-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}