{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T09:55:20Z","timestamp":1742982920232,"version":"3.40.3"},"publisher-location":"Singapore","reference-count":20,"publisher":"Springer Nature Singapore","isbn-type":[{"type":"print","value":"9789819616206"},{"type":"electronic","value":"9789819616213"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-981-96-1621-3_15","type":"book-chapter","created":{"date-parts":[[2025,2,24]],"date-time":"2025-02-24T08:15:30Z","timestamp":1740384930000},"page":"226-244","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Relational Denotational and\u00a0Algebraic Semantics Based on\u00a0UTP"],"prefix":"10.1007","author":[{"given":"Zhiru","family":"Hou","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,2,25]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, pp. 11\u201320 (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Chaudhuri, S., Gulwani, S., Lublinerman, R.: Continuity analysis of programs. In: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 57\u201370 (2010)","DOI":"10.1145\/1706299.1706308"},{"issue":"6","key":"15_CR3","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010)","journal-title":"J. Comput. Secur."},{"issue":"6","key":"15_CR4","doi-asserted-by":"publisher","first-page":"1207","DOI":"10.1017\/S0960129511000193","volume":"21","author":"G Barthe","year":"2011","unstructured":"Barthe, G., D\u2019argenio, P.R., Rezk, T.: Secure information flow by self-composition. Math. Struct. Comput. Sci. 21(6), 1207\u20131252 (2011)","journal-title":"Math. Struct. Comput. Sci."},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Darvas, \u00c1., H\u00e4hnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. In: Security in Pervasive Computing: Second International Conference, pp. 193\u2013209 (2005)","DOI":"10.1007\/978-3-540-32004-3_20"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: International Symposium on Formal Methods, pp. 200\u2013214 (2011)","DOI":"10.1007\/978-3-642-21437-0_17"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Churchill, B., Padon, O., Sharma, R., Aiken, A.: Semantic program alignment for equivalence checking. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 1027\u20131040 (2019)","DOI":"10.1145\/3314221.3314596"},{"issue":"1","key":"15_CR8","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/982962.964003","volume":"39","author":"N Benton","year":"2004","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. ACM SIGPLAN Not. 39(1), 14\u201325 (2004)","journal-title":"ACM SIGPLAN Not."},{"issue":"1","key":"15_CR9","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1145\/1111320.1111046","volume":"41","author":"T Amtoft","year":"2006","unstructured":"Amtoft, T., Bandhakavi, S., Banerjee, A.: A logic for information flow in object-oriented programs. ACM SIGPLAN Not. 41(1), 91\u2013102 (2006)","journal-title":"ACM SIGPLAN Not."},{"key":"15_CR10","volume-title":"Unifying Theories of Programming","author":"CAR Hoare","year":"1998","unstructured":"Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall, Englewood Cliffs (1998)"},{"key":"15_CR11","volume-title":"Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory","author":"JE Stoy","year":"1981","unstructured":"Stoy, J.E.: Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge (1981)"},{"issue":"8","key":"15_CR12","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/27651.27653","volume":"30","author":"CAR Hoare","year":"1987","unstructured":"Hoare, C.A.R., et al.: Laws of programming. Commun. ACM 30(8), 672\u2013686 (1987)","journal-title":"Commun. ACM"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Barthe, G., Eilers, R., Georgiou, P., Gleiss, B., Kov\u00e1cs, L., Maffei, M.: Verifying relational properties using trace logic. In: 2019 Formal Methods in Computer Aided Design (FMCAD), pp. 170\u2013178 (2019)","DOI":"10.23919\/FMCAD.2019.8894277"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Dardinier, T., M\u00fcller, P.: Hyper Hoare Logic: (dis-) proving program hyperproperties (extended version). arXiv:2301.10037 (2023)","DOI":"10.1145\/3656437"},{"issue":"3","key":"15_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3295699","volume":"28","author":"F Sheng","year":"2019","unstructured":"Sheng, F., Zhu, H., He, J., Yang, Z., Bowen, J.P.: Theoretical and practical aspects of linking operational and algebraic semantics for MDESL. ACM Trans. Softw. Eng. Methodol. (TOSEM) 28(3), 1\u201346 (2019)","journal-title":"ACM Trans. Softw. Eng. Methodol. (TOSEM)"},{"key":"15_CR16","unstructured":"Huet, G., Kahn, G., Paulin-Mohring, C.: The Coq Proof Assistant a Tutorial (2005)"},{"key":"15_CR17","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2013","unstructured":"Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2013)"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Naumann, D.A.: Thirty-seven years of relational Hoare logic: remarks on its principles and history. In: Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles: 9th International Symposium on Leveraging Applications of Formal Methods, pp. 93\u2013116 (2020)","DOI":"10.1007\/978-3-030-61470-6_7"},{"issue":"5","key":"15_CR19","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/360051.360056","volume":"19","author":"DE Denning","year":"1976","unstructured":"Denning, D.E.: A lattice model of secure information flow. Commun. ACM 19(5), 236\u2013243 (1976)","journal-title":"Commun. ACM"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Olderog, E.R.: Concurrent hyperproperties. In: Theories of Programming and Formal Methods: Essays Dedicated to Jifeng He on the Occasion of His 80th Birthday, pp. 211\u2013231 (2023)","DOI":"10.1007\/978-3-031-40436-8_8"}],"container-title":["Lecture Notes in Computer Science","Software Fault Prevention, Verification, and Validation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-96-1621-3_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,24]],"date-time":"2025-02-24T08:15:38Z","timestamp":1740384938000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-96-1621-3_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9789819616206","9789819616213"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-981-96-1621-3_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"25 February 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SFPVV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Software Fault Prevention, Verification, and Validation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hiroshima","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 December 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 December 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sfpvv2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}