{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,20]],"date-time":"2026-02-20T19:05:07Z","timestamp":1771614307433,"version":"3.50.1"},"reference-count":67,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2025,1,25]],"date-time":"2025-01-25T00:00:00Z","timestamp":1737763200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["#U2341212, #62132014"],"award-info":[{"award-number":["#U2341212, #62132014"]}],"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. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2025,2,28]]},"abstract":"<jats:p>\n            Complex safety-critical systems require multiple models for a comprehensive description, resulting in error-prone development and laborious verification. Bidirectional transformation (BX) is an approach to automatically synchronizing these models. However, existing BX frameworks lack formal verification to enforce these models\u2019 consistency rigorously. This paper introduces KBX, a formal bidirectional transformation framework for verified model synchronization. First, we present a matching logic-based BX model, providing a logical foundation for constructing BX definitions within the\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\mathbb{K}\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            framework. Second, we propose algorithms to synthesize formal BX definitions from unidirectional ones, which allows developers to focus on crafting the unidirectional definitions while disregarding the reverse direction and missing information recovery for synchronization. Afterward, we harness\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\mathbb{K}\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            to generate a formal synchronizer from the synthesized definitions for consistency maintenance and verification. To evaluate the effectiveness of KBX, we conduct a comparative analysis against existing BX frameworks. Furthermore, we demonstrate the application of KBX in constructing a BX between UML and HCSP for real-world scenarios, showcasing an 72% reduction in BX development effort compared to manual specification writing in\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\mathbb{K}\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            .\n          <\/jats:p>","DOI":"10.1145\/3696000","type":"journal-article","created":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T13:56:18Z","timestamp":1726235778000},"page":"1-40","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["KBX: Verified Model Synchronization via Formal Bidirectional Transformation"],"prefix":"10.1145","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-6524-1759","authenticated-orcid":false,"given":"Jianhong","family":"Zhao","sequence":"first","affiliation":[{"name":"Zhejiang University, Hangzhou, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2284-1383","authenticated-orcid":false,"given":"Yongwang","family":"Zhao","sequence":"additional","affiliation":[{"name":"Zhejiang University, Hangzhou, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0342-9518","authenticated-orcid":false,"given":"Peisen","family":"Yao","sequence":"additional","affiliation":[{"name":"Zhejiang University, Hangzhou, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6606-1602","authenticated-orcid":false,"given":"Fanlang","family":"Zeng","sequence":"additional","affiliation":[{"name":"Zhejiang University, Hangzhou, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5377-9351","authenticated-orcid":false,"given":"Bohua","family":"Zhan","sequence":"additional","affiliation":[{"name":"Institute of Software Chinese Academy of Sciences, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3441-6277","authenticated-orcid":false,"given":"Kui","family":"Ren","sequence":"additional","affiliation":[{"name":"Zhejiang University, Hangzhou, China"}]}],"member":"320","published-online":{"date-parts":[[2025,1,25]]},"reference":[{"issue":"3","key":"e_1_3_2_2_1","doi-asserted-by":"crossref","first-page":"235","DOI":"10.3233\/FI-2020-1989","article-title":"Abstract contract synthesis and verification in the symbolic K framework","volume":"177","author":"Alpuente Mar\u00eda","year":"2020","unstructured":"Mar\u00eda Alpuente, Daniel Pardo, and Alicia Villanueva. 2020. Abstract contract synthesis and verification in the symbolic K framework. Fundamenta Informaticae 177, 3-4 (Dec. 2020), 235\u2013273. Retrieved from https:\/\/www.medra.org\/servlet\/aliasResolver?alias=iospress{&}doi=10.3233\/FI-2020-1989","journal-title":"Fundamenta Informaticae"},{"issue":"3","key":"e_1_3_2_3_1","first-page":"647","article-title":"Benchmarking bidirectional transformations: Theory, implementation","volume":"19","author":"Anjorin Anthony","year":"2020","unstructured":"Anthony Anjorin, Thomas Buchmann, Bernhard Westfechtel, Zinovy Diskin, Hsiang-Shang Ko, Romina Eramo, Georg Hinkel, Leila Samimi-Dehkordi, and Albert Z\u00fcndorf. 2020. Benchmarking bidirectional transformations: Theory, implementation, application, and assessment. Software and Systems Modeling 19, 3 (2020), 647\u2013691.","journal-title":"application, and assessment. Software and Systems Modeling"},{"key":"e_1_3_2_4_1","volume-title":"Refinement Calculus: A Systematic Introduction","author":"Back Ralph-Johan","year":"2012","unstructured":"Ralph-Johan Back and Joakim Wright. 2012. Refinement Calculus: A Systematic Introduction. Springer Science & Business Media."},{"key":"e_1_3_2_5_1","doi-asserted-by":"crossref","first-page":"386","DOI":"10.1007\/978-3-031-13188-2_19","volume-title":"Computer Aided Verification","author":"Bang Seongwon","year":"2022","unstructured":"Seongwon Bang, Seunghyeon Nam, Inwhan Chun, Ho Young Jhoo, and Juneyoung Lee. 2022. SMT-based translation validation for machine learning compiler. In Computer Aided Verification. S. Shoham and Y. Vizel (Eds.), Springer, 386\u2013407. Retrieved from https:\/\/link.springer.com\/chapter\/10.1007\/978-3-031-13188-2_19"},{"key":"e_1_3_2_6_1","first-page":"3","volume-title":"ACM International Conference Proceeding Series","volume":"162","author":"Bell Ron","year":"2006","unstructured":"Ron Bell. 2006. Introduction to IEC 61508. In ACM International Conference Proceeding Series, Vol. 162, 3\u201312."},{"key":"e_1_3_2_7_1","volume-title":"Implementing Domain-Specific Languages with Xtext and Xtend: Learn How to Implement a DSL with Xtext and Xtend Using Easy-to-Understand Examples and Best Practices (2nd. ed.)","author":"Bettini Lorenzo","year":"2016","unstructured":"Lorenzo Bettini and Sven Efftinge. 2016. Implementing Domain-Specific Languages with Xtext and Xtend: Learn How to Implement a DSL with Xtext and Xtend Using Easy-to-Understand Examples and Best Practices (2nd. ed.). Packt Publishing, Birmingham Mumbai."},{"key":"e_1_3_2_8_1","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1145\/2676726.2676982","volume-title":"Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Bogdanas Denis","year":"2015","unstructured":"Denis Bogdanas and Grigore Ro\u015fu. 2015. K-Java: A complete semantics of java. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, Mumbai India, 445\u2013456. Retrieved from https:\/\/dl.acm.org\/doi\/10.1145\/2676726.2676982"},{"key":"e_1_3_2_9_1","doi-asserted-by":"crossref","first-page":"336","DOI":"10.5220\/0006563503360345","volume-title":"Proceedings of the 6th International Conference on Model-Driven Engineering and Software Developme (MODELSWARD \u201918)","author":"Buchmann Thomas","year":"2018","unstructured":"Thomas Buchmann. 2018. BXtend-A framework for (bidirectional) incremental model transformations.. In Proceedings of the 6th International Conference on Model-Driven Engineering and Software Developme (MODELSWARD \u201918), 336\u2013345."},{"key":"e_1_3_2_10_1","doi-asserted-by":"crossref","unstructured":"Thomas Buchmann Matthias Bank and Bernhard Westfechtel. 2022. BXtendDSL: A layered framework for bidirectional model transformations combining a declarative and an imperative language. Journal of Systems and Software 189 (July 2022) 111288. Retrieved from https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0164121222000462","DOI":"10.1016\/j.jss.2022.111288"},{"key":"e_1_3_2_11_1","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1007\/BFb0020972","volume-title":"Hybrid Systems III: Verification and Control","author":"Chaochen Zhou","year":"1996","unstructured":"Zhou Chaochen, Wang Ji, and Anders P. Ravn. 1996. A formal description of hybrid systems. In Hybrid Systems III: Verification and Control 3. Rajeev Alur, Thomas A. Henzinger, and Eduardo D. Sontag (Eds.),Springer, 511\u2013530."},{"issue":"1","key":"e_1_3_2_12_1","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/s10817-017-9446-0","article-title":"Toward compositional verification of interruptible Os kernels and device drivers","volume":"61","author":"Chen Hao","year":"2018","unstructured":"Hao Chen, Xiongnan Wu, Zhong Shao, Joshua Lockerman, and Ronghui Gu. 2018. Toward compositional verification of interruptible Os kernels and device drivers. Journal of Automated Reasoning 61, 1 (2018), 141\u2013189.","journal-title":"Journal of Automated Reasoning"},{"key":"e_1_3_2_13_1","doi-asserted-by":"crossref","first-page":"477","DOI":"10.1007\/978-3-030-81688-9_23","volume-title":"Computer Aided Verification, Lecture Notes in Computer Science","author":"Chen Xiaohong","year":"2021","unstructured":"Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh, and Grigore Ro\u015fu. 2021a. Towards a trustworthy semantics-based language framework via proof generation. In Computer Aided Verification, Lecture Notes in Computer Science.Alexandra Silva and K. R. M. Leino (Eds.), Springer International Publishing, Cham, 477\u2013499."},{"key":"e_1_3_2_14_1","doi-asserted-by":"crossref","unstructured":"Xiaohong Chen Dorel Lucanu and Grigore Ro\u015fu. 2021b. Matching logic explained. Journal of Logical and Algebraic Methods in Programming 120 (April 2021) 100638. Retrieved from https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S2352220821000018","DOI":"10.1016\/j.jlamp.2021.100638"},{"key":"e_1_3_2_15_1","first-page":"1","volume-title":"Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201919)","author":"Chen Xiaohong","year":"2019","unstructured":"Xiaohong Chen and Grigore Ro\u015fu. 2019. Matching \\(\\mu\\) -logic. In Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201919). IEEE, 1\u201313."},{"key":"e_1_3_2_16_1","volume-title":"Proceedings of the 8th Conference on Algebra and Coalgebra in Computer Science (CALCO \u201919)","author":"Chen Xiaohong","year":"2019","unstructured":"Xiaohong Chen and Grigore Rosu. 2019. Matching mu-logic: Foundation of K framework. In Proceedings of the 8th Conference on Algebra and Coalgebra in Computer Science (CALCO \u201919). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik."},{"key":"e_1_3_2_17_1","first-page":"183","volume-title":"Software Language Engineering, Lecture Notes in Computer Science","author":"Cicchetti Antonio","year":"2011","unstructured":"Antonio Cicchetti, Davide Di Ruscio, Romina Eramo, and Alfonso Pierantonio. 2011. JTL: A bidirectional and change propagating transformation language. In Software Language Engineering, Lecture Notes in Computer Science. Brian Malloy, Steffen Staab, and Mark van den Brand (Eds.), Springer, Berlin, 183\u2013202."},{"key":"e_1_3_2_18_1","doi-asserted-by":"crossref","first-page":"1133","DOI":"10.1145\/3314221.3314601","volume-title":"Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"Dasgupta Sandeep","year":"2019","unstructured":"Sandeep Dasgupta, Daejun Park, Theodoros Kasampalis, Vikram S. Adve, and Grigore Ro\u015fu. 2019. A complete formal semantics of X86-64 user-level instruction set architecture. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, 1133\u20131148. Retrieved from https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314601"},{"key":"e_1_3_2_19_1","first-page":"533","volume-title":"SIGPLAN Notices","volume":"47","author":"Ellison Chucky","year":"2012","unstructured":"Chucky Ellison and Grigore Rosu. 2012. An executable formal semantics of C with applications. SIGPLAN Notices 47, 1 (Jan 2012), 533\u2013544. DOI:10.1145\/2103621.2103719"},{"key":"e_1_3_2_20_1","unstructured":"Chucky M. Ellison and Grigore Ro\u015fu. 2011. An executable formal semantics of C with applications: Technical report. ACM SIGPLAN Notices (2011). Retrieved from http:\/\/www.researchgate.net\/publication\/49175991_A_Formal_Semantics_of_C_with_Applications_Technical_Report"},{"key":"e_1_3_2_21_1","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1145\/3191697.3191720","volume-title":"Proceedings of the Conference Companion of the 2nd International Conference on Art, Science, and Engineering of Programming","author":"Eramo Romina","year":"2018","unstructured":"Romina Eramo, Alfonso Pierantonio, and Michele Tucci. 2018. Enhancing the JTL tool for bidirectional transformations. In Proceedings of the Conference Companion of the 2nd International Conference on Art, Science, and Engineering of Programming. ACM, 36\u201341. Retrieved from https:\/\/dl.acm.org\/doi\/10.1145\/3191697.3191720"},{"key":"e_1_3_2_22_1","doi-asserted-by":"crossref","unstructured":"Chris Hathhorn Chucky Ellison and Grigore Ro?u. 2015. Defining the undefinedness of C. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM 336\u2013345. Retrieved from http:\/\/dl.acm.org\/doi\/abs\/10.1145\/2737924.2737979","DOI":"10.1145\/2737924.2737979"},{"key":"e_1_3_2_23_1","doi-asserted-by":"crossref","first-page":"668","DOI":"10.1007\/978-3-642-24485-8_49","volume-title":"Model Driven Engineering Languages and Systems","author":"Hermann Frank","year":"2011","unstructured":"Frank Hermann, Hartmut Ehrig, Fernando Orejas, Krzysztof Czarnecki, Zinovy Diskin, and Yingfei Xiong. 2011. Correctness of model synchronization based on triple graph grammars. In Model Driven Engineering Languages and Systems. Jon Whittle, Tony Clark and Thomas K\u00fchne (Eds.), Vol. 6981. Springer, Berlin, 668\u2013682. Retrieved from http:\/\/link.springer.com\/10.1007\/978-3-642-24485-8_49"},{"issue":"3","key":"e_1_3_2_24_1","doi-asserted-by":"crossref","first-page":"907","DOI":"10.1007\/s10270-014-0450-0","article-title":"Feature-based classification of bidirectional transformation approaches","volume":"15","author":"Hidaka Soichiro","year":"2016","unstructured":"Soichiro Hidaka, Massimo Tisi, Jordi Cabot, and Zhenjiang Hu. 2016. Feature-based classification of bidirectional transformation approaches. Software & Systems Modeling 15, 3 (July 2016), 907\u2013928. Retrieved from http:\/\/link.springer.com\/10.1007\/s10270-014-0450-0","journal-title":"Software & Systems Modeling"},{"key":"e_1_3_2_25_1","first-page":"865","article-title":"A survey of triple graph grammar tools","volume":"57","author":"Hildebrandt Stephan","year":"2013","unstructured":"Stephan Hildebrandt, Leen Lambers, Holger Giese, Jan Rieke, Joel Greenyer, Wilhelm Sch\u00e4fer, Marius Lauder, Anthony Anjorin, and Andy Sch\u00fcrr. 2013. A survey of triple graph grammar tools. Electronic Communications of the EASST 57 (2013), 865. Retrieved from https:\/\/eceasst.org\/index.php\/eceasst\/article\/view\/2083","journal-title":"Electronic Communications of the EASST"},{"issue":"1","key":"e_1_3_2_26_1","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/s10270-017-0617-6","article-title":"Change propagation and bidirectionality in internal transformation DSLs","volume":"18","author":"Hinkel Georg","year":"2019","unstructured":"Georg Hinkel and Erik Burger. 2019. Change propagation and bidirectionality in internal transformation DSLs. Software & Systems Modeling 18, 1 (2019), 249\u2013278.","journal-title":"Software & Systems Modeling"},{"issue":"1","key":"e_1_3_2_27_1","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1145\/1925844.1926428","article-title":"Symmetric lenses","volume":"46","author":"Hofmann Martin","year":"2011","unstructured":"Martin Hofmann, Benjamin Pierce, and Daniel Wagner. 2011. Symmetric lenses. ACM SIGPLAN Notices 46, 1 (2011), 371\u2013384.","journal-title":"ACM SIGPLAN Notices"},{"key":"e_1_3_2_28_1","first-page":"100","volume-title":"Bidirectional Transformations","author":"Hu Zhenjiang","year":"2018","unstructured":"Zhenjiang Hu and Hsiang-Shang Ko. 2018. Principles and practice of bidirectional programming in BiGUL. In Bidirectional Transformations. Jeremy Gibbons and Perdita Stevens (Eds.), Vol. 9715. Springer International Publishing, 100\u2013150. Retrieved from http:\/\/link.springer.com\/10.1007\/978-3-319-79108-1_4"},{"key":"e_1_3_2_29_1","volume-title":"Infotech@Aerospace 2012","author":"Jacklin Stephen","year":"2012","unstructured":"Stephen Jacklin. 2012. Certification of safety-critical software under DO-178C and DO-278A. In Infotech@Aerospace 2012. American Institute of Aeronautics and Astronautics, Retrieved from https:\/\/arc.aiaa.org\/doi\/10.2514\/6.2012-2473"},{"key":"e_1_3_2_30_1","first-page":"31","article-title":"Bidirectional certified programming","author":"Kinoshita Daisuke","year":"2017","unstructured":"Daisuke Kinoshita and Keisuke Nakano. 2017. Bidirectional certified programming. In BX@ ETAPS, 31\u201338.","journal-title":"BX@ ETAPS"},{"key":"e_1_3_2_31_1","doi-asserted-by":"crossref","first-page":"110815","DOI":"10.1016\/j.jss.2020.110815","article-title":"Enabling consistency in view-based system development\u2014The vitruvius approach","volume":"171","author":"Klare Heiko","year":"2021","unstructured":"Heiko Klare, Max E. Kramer, Michael Langhammer, Dominik Werle, Erik Burger, and Ralf Reussner. 2021. Enabling consistency in view-based system development\u2014The vitruvius approach. Journal of Systems and Software 171 2021), 110815.","journal-title":"Journal of Systems and Software"},{"key":"e_1_3_2_32_1","unstructured":"Gerwin Klein June Andronick Kevin Elphinstone Toby Murray Thomas Sewell Rafal Kolanski and Gernot Heiser. 2014. Comprehensive Formal Verification of an OS Microkernel. (2014). Retrieved from http:\/\/trustworthy.systems\/publications\/nictaabstracts\/Klein_AEMSKH_14.abstract \/publications\/nictaabstracts\/Klein_AEMSKH_14.abstract"},{"key":"e_1_3_2_33_1","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1007\/978-1-4419-1539-9_11","volume-title":"Design and Verification of Microprocessor Systems for High-Assurance Applications","author":"Klein Gerwin","year":"2010","unstructured":"Gerwin Klein, Thomas Sewell, and Simon Winwood. 2010. Refinement in the formal verification of the seL4 microkernel. In Design and Verification of Microprocessor Systems for High-Assurance Applications. Rockwell Collins and David S. Hardin (Eds.), Springer, 323\u2013339."},{"key":"e_1_3_2_34_1","first-page":"61","volume-title":"Proceedings of the 2016 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation","author":"Ko Hsiang-Shang","year":"2016","unstructured":"Hsiang-Shang Ko, Tao Zan, and Zhenjiang Hu. 2016. BiGUL: A formally verified core language for putback-based bidirectional programming. In Proceedings of the 2016 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation. ACM, 61\u201372. Retrieved from https:\/\/dl.acm.org\/doi\/10.1145\/2847538.2847544"},{"issue":"3","key":"e_1_3_2_35_1","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","article-title":"Results on the propositional  \\(\\mu\\)","volume":"27","author":"Kozen Dexter","year":"1983","unstructured":"Dexter Kozen. 1983. Results on the propositional \\(\\mu\\) -calculus. Theoretical Computer Science 27, 3 (1983), 333\u2013354.","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"e_1_3_2_36_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3522582","article-title":"A survey of practical formal methods for security","volume":"34","author":"Kulik Tomas","year":"2022","unstructured":"Tomas Kulik, Brijesh Dongol, Peter Gorm Larsen, Hugo Daniel Macedo, Steve Schneider, Peter W. V. Tran-J\u00f8rgensen, and James Woodcock. 2022. A survey of practical formal methods for security. Formal Aspects of Computing 34, 1 (2022), 1\u201339.","journal-title":"Formal Aspects of Computing"},{"key":"e_1_3_2_37_1","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/s00165-014-0313-z","article-title":"A framework for model transformation verification","volume":"27","author":"Lano Kevin","year":"2015","unstructured":"Kevin Lano, Tony Clark, and S. Kolahdouz-Rahimi. 2015. A framework for model transformation verification. Formal Aspects of Computing 27 (2015), 193\u2013235.","journal-title":"Formal Aspects of Computing"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","unstructured":"Dirk Carsten Leinenbach. 2008. Compiler Verification in the Context of Pervasive System Verification. Ph.D. Dissertation. Saarland University Saarbr\u00fccken Germany. Retrieved from https:\/\/doi.org\/10.22028\/D291-25991","DOI":"10.22028\/D291-25991"},{"key":"e_1_3_2_39_1","doi-asserted-by":"crossref","first-page":"386","DOI":"10.1007\/978-3-642-35182-2_27","volume-title":"Proceedings of the Programming Languages and Systems: 10th Asian Symposium (APLAS \u201912)","author":"Leroy Xavier","year":"2012","unstructured":"Xavier Leroy. 2012. Mechanized semantics for compiler verification. In Proceedings of the Programming Languages and Systems: 10th Asian Symposium (APLAS \u201912). Springer, 386\u2013388."},{"key":"e_1_3_2_40_1","first-page":"1782","volume-title":"Proceedings of the IEEE Symposium on Security and Privacy (SP \u201921)","author":"Li Shih-Wei","year":"2021","unstructured":"Shih-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, and John Zhuang Hui. 2021. A secure and formally verified linux KVM hypervisor. In Proceedings of the IEEE Symposium on Security and Privacy (SP \u201921). IEEE, 1782\u20131799. Retrieved from https:\/\/ieeexplore.ieee.org\/document\/9519433\/"},{"key":"e_1_3_2_41_1","first-page":"56","volume-title":"Proceedings of the ACM on Programming Languages","volume":"7","author":"Lin Zhengyao","year":"2023","unstructured":"Zhengyao Lin, Xiaohong Chen, Minh-Thai Trinh, John Wang, and Grigore Ro\u015fu. 2023. Generating proof certificates for a language-agnostic deductive program verifier. Proceedings of the ACM on Programming Languages 7, OOPSLA1 (April 2023), 56\u201384. Retrieved from https:\/\/dl.acm.org\/doi\/10.1145\/3586029"},{"key":"e_1_3_2_42_1","first-page":"1","volume-title":"Proceedings of the Programming Languages and Systems: 8th Asian Symposium (APLAS \u201910)","author":"Liu Jiang","year":"2010","unstructured":"Jiang Liu, Jidong Lv, Zhao Quan, Naijun Zhan, Hengjun Zhao, Chaochen Zhou, and Liang Zou. 2010. A calculus for hybrid CSP. In Proceedings of the Programming Languages and Systems: 8th Asian Symposium (APLAS \u201910). Springer, 1\u201315."},{"key":"e_1_3_2_43_1","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1145\/3453483.3454030","volume-title":"Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","author":"Lopes Nuno P.","year":"2021","unstructured":"Nuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, and John Regehr. 2021. Alive2: Bounded translation validation for LLVM. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. ACM, 65\u201379. Retrieved from https:\/\/dl.acm.org\/doi\/10.1145\/3453483.3454030"},{"key":"e_1_3_2_44_1","first-page":"1","volume-title":"Proceedings of the ACM on Programming Languages","volume":"4","author":"Lubin Justin","year":"2020","unstructured":"Justin Lubin, Nick Collins, Cyrus Omar, and Ravi Chugh. 2020. Program sketching with live bidirectional evaluation. Proceedings of the ACM on Programming Languages 4, ICFP (August 2020), 1\u201329. Retrieved from https:\/\/dl.acm.org\/doi\/10.1145\/3408991"},{"key":"e_1_3_2_45_1","first-page":"1","volume-title":"Proceedings of the ACM on Programming Languages","volume":"2","author":"Maina Solomon","year":"2018","unstructured":"Solomon Maina, Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic. 2018. Synthesizing quotient lenses. Proceedings of the ACM on Programming Languages 2, ICFP (July 2018), 1\u201329. Retrieved from https:\/\/dl.acm.org\/doi\/10.1145\/3236775"},{"key":"e_1_3_2_46_1","first-page":"31","volume-title":"Proceedings of the European Symposium on Programming","author":"Matsuda Kazutaka","year":"2018","unstructured":"Kazutaka Matsuda and Meng Wang. 2018. Hobit: Programming lenses without using lens combinators. In Proceedings of the European Symposium on Programming. Springer, 31\u201359."},{"key":"e_1_3_2_47_1","first-page":"1","volume-title":"Proceedings of the ACM on Programming Languages","volume":"2","author":"Mayer Mika\u00ebl","year":"2018","unstructured":"Mika\u00ebl Mayer, Viktor Kuncak, and Ravi Chugh. 2018. Bidirectional evaluation with direct manipulation. Proceedings of the ACM on Programming Languages 2, OOPSLA (October 2018), 1\u201328. Retrieved from https:\/\/dl.acm.org\/doi\/10.1145\/3276497"},{"key":"e_1_3_2_48_1","first-page":"1","volume-title":"Proceedings of the ACM on Programming Languages","volume":"2","author":"Miltner Anders","year":"2018","unstructured":"Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic. 2018. Synthesizing bijective lenses. Proceedings of the ACM on Programming Languages 2, POPL (January 2018), 1\u201330. Retrieved from https:\/\/dl.acm.org\/doi\/10.1145\/3158089"},{"key":"e_1_3_2_49_1","first-page":"1","volume-title":"Proceedings of the ACM on Programming Languages","volume":"3","author":"Miltner Anders","year":"2019","unstructured":"Anders Miltner, Solomon Maina, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic. 2019. Synthesizing symmetric lenses. Proceedings of the ACM on Programming Languages 3, ICFP (July 2019), 1\u201328. Retrieved from https:\/\/dl.acm.org\/doi\/10.1145\/3341699"},{"key":"e_1_3_2_50_1","volume-title":"On the Refinement Calculus. Number 70 in Technical Monograph \/ Oxford Univ","author":"Morgan Carroll","year":"1988","unstructured":"Carroll Morgan, Ken Robinson, and Paul Gardiner. 1988. On the Refinement Calculus. Number 70 in Technical Monograph \/ Oxford Univ. Computing Laboratory, Programming Research Group. University Computing Laboratory, Oxford."},{"key":"e_1_3_2_51_1","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1145\/2737924.2737991","volume-title":"Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201915)","author":"Park Daejun","year":"2015","unstructured":"Daejun Park, Andrei Stef\u0103nescu, and Grigore Ro\u015fu. 2015. KJS: A complete formal semantics of JavaScript. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201915). Association for Computing Machinery, New York, NY, 346\u2013356. DOI:10.1145\/2737924.2737991"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","unstructured":"Alastair Reid Luke Church Shaked Flur Sarah de Haas Maritza Johnson and Ben Laurie. 2020. Towards making formal methods normal: Meeting developers where they are. arXiv:2010.16345. Retrieved from https:\/\/doi.org\/10.48550\/arXiv.2010.16345","DOI":"10.48550\/arXiv.2010.16345"},{"key":"e_1_3_2_53_1","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/j.infsof.2018.03.011","article-title":"EVL+Strace: A novel bidirectional model transformation approach","volume":"100","author":"Samimi-Dehkordi Leila","year":"2018","unstructured":"Leila Samimi-Dehkordi, Bahman Zamani, and Shekoufeh Kolahdouz-Rahimi. 2018. EVL+Strace: A novel bidirectional model transformation approach. Information and Software Technology 100 (August 2018), 47\u201372. Retrieved from https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0950584917300629","journal-title":"Information and Software Technology"},{"key":"e_1_3_2_54_1","doi-asserted-by":"crossref","first-page":"471","DOI":"10.1145\/2491956.2462183","volume-title":"Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"Sewell Thomas Arthur Leck","year":"2013","unstructured":"Thomas Arthur Leck Sewell, Magnus O. Myreen, and Gerwin Klein. 2013. Translation validation for a verified OS kernel. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, 471\u2013482."},{"key":"e_1_3_2_55_1","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1145\/1706299.1706337","volume-title":"Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Srivastava Saurabh","year":"2010","unstructured":"Saurabh Srivastava, Sumit Gulwani, and Jeffrey S. Foster. 2010. From program verification to program synthesis. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 313\u2013326."},{"key":"e_1_3_2_56_1","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1145\/2983990.2984027","volume-title":"Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications","author":"Stef\u0103nescu Andrei","year":"2016","unstructured":"Andrei Stef\u0103nescu, Daejun Park, Shijiao Yuwen, Yilong Li, and Grigore Ro\u015fu. 2016. Semantics-based program verifiers for all languages. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications. ACM, 74\u201391. Retrieved from https:\/\/dl.acm.org\/doi\/10.1145\/2983990.2984027"},{"key":"e_1_3_2_57_1","doi-asserted-by":"crossref","first-page":"408","DOI":"10.1007\/978-3-540-88643-3_10","volume-title":"Generative and Transformational Techniques in Software Engineering II","author":"Stevens. Perdita","year":"2008","unstructured":"Perdita Stevens. 2008. A landscape of bidirectional model transformations. In Generative and Transformational Techniques in Software Engineering II. Ralf L\u00e4mmel, Joost Visser, and Jo\u00e3o Saraiva (Eds.), Vol. 5235. Springer, Berlin, 408\u2013424. Retrieved from http:\/\/link.springer.com\/10.1007\/978-3-540-88643-3_10"},{"key":"e_1_3_2_58_1","volume-title":"Proceedings of the Eighth International Workshop on Bidirectional Transformations","author":"Weidmann Nils","year":"2019","unstructured":"Nils Weidmann, Anthony Anjorin, Gergely Varro, Lars Fritsche, Andy Schurr, and Erhan Leblebici. 2019. Incremental bidirectional model transformation with eMoflon::IBeX. In Proceedings of the Eighth International Workshop on Bidirectional Transformations. Retrieved from http:\/\/ceur-ws.org"},{"key":"e_1_3_2_59_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-29044-2","volume-title":"Experimentation in Software Engineering","author":"Wohlin Claes","year":"2012","unstructured":"Claes Wohlin, Per Runeson, Martin H\u00f6st, Magnus C. Ohlsson, Bj\u00f6rn Regnell, and Anders Wessl\u00e9n. 2012. Experimentation in Software Engineering. Vol. 236. Springer."},{"key":"e_1_3_2_60_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.tcs.2021.11.008","article-title":"Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and simulink\/stateflow","volume":"903","author":"Xu Xiong","year":"2022","unstructured":"Xiong Xu, Shuling Wang, Bohua Zhan, Xiangyu Jin, Jean-Pierre Talpin, and Naijun Zhan. 2022. Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and simulink\/stateflow. Theoretical Computer Science 903 (2022), 1\u201325.","journal-title":"Theoretical Computer Science"},{"key":"e_1_3_2_61_1","doi-asserted-by":"crossref","unstructured":"Masaomi Yamaguchi Kazutaka Matsuda Cristina David and Meng Wang. 2021. Synbit: Synthesizing bidirectional programs using unidirectional sketches. arXiv:2108.13783 [cs]. Retrieved from http:\/\/arxiv.org\/abs\/2108.13783","DOI":"10.1145\/3485482"},{"key":"e_1_3_2_62_1","first-page":"457","volume-title":"Proceedings of the IEEE 27th Real-Time and Embedded Technology and Applications Symposium (RTAS \u201921)","author":"Zhan Bohua","year":"2021","unstructured":"Bohua Zhan, Bin Gu, Xiong Xu, Xiangyu Jin, Shuling Wang, Bai Xue, Xiaofeng Li, Yao Chen, Mengfei Yang, and Naijun Zhan. 2021. Brief industry paper: Modeling and verification of descent guidance control of mars lander. In Proceedings of the IEEE 27th Real-Time and Embedded Technology and Applications Symposium (RTAS \u201921). IEEE, 457\u2013460."},{"key":"e_1_3_2_63_1","first-page":"230","volume-title":"Proceedings of the ACM on Programming Languages","volume":"7","author":"Zhang Xing","year":"2023","unstructured":"Xing Zhang, Guanchen Guo, Xiao He, and Zhenjiang Hu. 2023. Bidirectional object-oriented programming: towards programmatic and direct manipulation of objects. Proceedings of the ACM on Programming Languages 7, OOPSLA1 (April 2023), 230\u2013255. Retrieved from https:\/\/dl.acm.org\/doi\/10.1145\/3586035"},{"key":"e_1_3_2_64_1","doi-asserted-by":"crossref","first-page":"2154","DOI":"10.1145\/3510003.3510195","volume-title":"Proceedings of the 44th International Conference on Software Engineering","author":"Zhang Xing","year":"2022","unstructured":"Xing Zhang and Zhenjiang Hu. 2022. Towards bidirectional live programming for incomplete programs. In Proceedings of the 44th International Conference on Software Engineering. ACM, 2154\u20132164. Retrieved from https:\/\/dl.acm.org\/doi\/10.1145\/3510003.3510195"},{"key":"e_1_3_2_65_1","volume-title":"Proceedings of the 4th International Workshop on Bidirectional Transformations","author":"Zhu Zirun","year":"2015","unstructured":"Zirun Zhu, Hsiang-Shang Ko, Pedro Miguel Ribeiro Martins, Jo\u00e3o Alexandre Saraiva, and Zhenjiang Hu. 2015. BiYacc: Roll your parser and reflective printer into one. In Proceedings of the 4th International Workshop on Bidirectional Transformations. CEUR-Ws. Retrieved from http:\/\/ceur-ws.org"},{"key":"e_1_3_2_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00354-019-00082-y"},{"key":"e_1_3_2_67_1","first-page":"464","volume-title":"Proceedings of the Automated Technology for Verification and Analysis: 13th International Symposium (ATVA \u201915)","author":"Zou Liang","year":"2015","unstructured":"Liang Zou, Naijun Zhan, Shuling Wang, and Martin Fr\u00e4nzle. 2015. Formal verification of simulink\/stateflow diagrams. In Proceedings of the Automated Technology for Verification and Analysis: 13th International Symposium (ATVA \u201915). Springer, 464\u2013481."},{"key":"e_1_3_2_68_1","first-page":"1","volume-title":"Proceedings of the International Conference on Embedded Software (EMSOFT \u201913)","author":"Zou Liang","year":"2013","unstructured":"Liang Zou, Naijun Zhany, Shuling Wang, Martin Fr\u00e4nzle, and Shengchao Qin. 2013. Verifying simulink diagrams via a hybrid hoare logic prover. In Proceedings of the International Conference on Embedded Software (EMSOFT \u201913). IEEE, 1\u201310."}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3696000","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3696000","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:04:30Z","timestamp":1750291470000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3696000"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,25]]},"references-count":67,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,2,28]]}},"alternative-id":["10.1145\/3696000"],"URL":"https:\/\/doi.org\/10.1145\/3696000","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,25]]},"assertion":[{"value":"2024-03-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-27","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-25","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}