{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,23]],"date-time":"2026-09-23T04:50:23Z","timestamp":1790139023519,"version":"4.0.1"},"reference-count":137,"publisher":"Association for Computing Machinery (ACM)","issue":"10","license":[{"start":{"date-parts":[[2025,5,7]],"date-time":"2025-05-07T00:00:00Z","timestamp":1746576000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Comput. Surv."],"published-print":{"date-parts":[[2025,10,31]]},"abstract":"<jats:p>Proof scores can be regarded as outlines of the formal verification of system properties. They have been historically used by the OBJ family of specification languages. The main advantage of proof scores is that they follow the same syntax as the specification language they are used in, so specifiers can easily adopt them and use as many features as the particular language provides. In this way, proof scores have been successfully used to prove properties of a large number of systems and protocols. However, proof scores also present a number of disadvantages that prevented a large audience from adopting them as proving mechanism.<\/jats:p>\n          <jats:p>In this article, we present the theoretical foundations of proof scores; the different systems where they have been adopted and their latest developments; the classes of systems successfully verified using proof scores, including the main techniques used for it; the main reasons why they have not been widely adopted; and finally we discuss some directions of future work that might solve the problems discussed previously.<\/jats:p>\n          <jats:p\/>","DOI":"10.1145\/3729166","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T10:01:51Z","timestamp":1744192911000},"page":"1-37","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Proof Scores: A Survey"],"prefix":"10.1145","volume":"57","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9716-4612","authenticated-orcid":false,"given":"Adri\u00e1n","family":"Riesco","sequence":"first","affiliation":[{"name":"Sistemas Inform\u00e1ticos y Computaci\u00f3n, Universidad Complutense de Madrid Facultad de Informatica, Madrid, Spain and Instituto de Tecnolog\u00eda del Conocimiento, Madrid, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4441-3259","authenticated-orcid":false,"given":"Kazuhiro","family":"Ogata","sequence":"additional","affiliation":[{"name":"Japan Advanced Institute of Science and Technology, Nomi, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6789-9688","authenticated-orcid":false,"given":"Masaki","family":"Nakamura","sequence":"additional","affiliation":[{"name":"Toyama Prefectural University, Imizu, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0978-2200","authenticated-orcid":false,"given":"Daniel","family":"Gaina","sequence":"additional","affiliation":[{"name":"Kyushu University, Fukuoka, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7092-2084","authenticated-orcid":false,"given":"Duong Dinh","family":"Tran","sequence":"additional","affiliation":[{"name":"Japan Advanced Institute of Science and Technology, Nomi, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5853-3243","authenticated-orcid":false,"given":"Kokichi","family":"Futatsugi","sequence":"additional","affiliation":[{"name":"Japan Advanced Institute of Science and Technology, Nomi, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,5,7]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0145-y"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575691"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2024.103088"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_9"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439934"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373829"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00368-1"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ITP.2021.4"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.02.006"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.29007\/432M"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/77600.77621"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100013463"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00206-6"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"e_1_3_3_20_2","volume-title":"Proceedings of the 5th International Joint Conference on Artificial Intelligence. William Kaufmann","author":"Rod","unstructured":"Rod M. Burstall and Joseph A. Goguen. 1977. Putting theories together to make specifications. In Proceedings of the 5th International Joint Conference on Artificial Intelligence. William Kaufmann, Burlington, Massachusetts, 1045\u20131058."},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10007-5_41"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/800087.802799"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3497775.3503681"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2403.14064"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ITP.2023.9"},{"key":"e_1_3_3_26_2","volume-title":"Peled","author":"Clarke Edmund M.","year":"1999","unstructured":"Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 1999. Model Checking. MIT Press, Cambridge, Massachusetts."},{"key":"e_1_3_3_27_2","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude: A High-Performance Logical Framework","author":"Clavel Manuel","unstructured":"Manuel Clavel, Francisco Dur\u00e1n, Steven Eker, Patrick Lincoln, Narciso Mart\u00ed-Oliet, Jos\u00e9 Meseguer, and Carolyn Talcott. 2007a. All About Maude: A High-Performance Logical Framework. Lecture Notes in Computer Science, Vol. 4350, Springer, Berlin."},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73859-6_12"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.3217\/jucs-012-11-1618"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17796-5_4"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2013.11.008"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","unstructured":"Leonardo Mendon\u00e7a de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An efficient SMT solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems Held as Part of the Joint European Conferences on Theory and Practice of Software ETAPS 2008. C. R. Ramakrishnan and Jakob Rehof (Eds.) Lecture Notes in Computer Science Vol. 4963 Springer Berlin 337\u2013340. DOI:10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_45"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.04.008"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.JLAMP.2014.03.001"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1142\/3831"},{"key":"e_1_3_3_37_2","first-page":"74","article-title":"Behavioural coherence in object-oriented algebraic specification","volume":"6","author":"Diaconescu Razvan","year":"2000","unstructured":"Razvan Diaconescu and Kokichi Futatsugi. 2000. Behavioural coherence in object-oriented algebraic specification. Journal of Universal Computer Science 6, 1 (2000), 74\u201396.","journal-title":"Journal of Universal Computer Science"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00361-9"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/3497775.3503692"},{"key":"e_1_3_3_40_2","unstructured":"Pablo Donato Benjamin Werner and Kaustuv Chaudhuri. 2023. Integrating graphical proofs in Coq. (2023). https:\/\/popl23.sigplan.org\/details\/CoqPL-2023-papers\/6\/Integrating-graphical-proofs-in-Coq"},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"e_1_3_3_43_2","volume-title":"Proceedings of the 2nd Workshop on Abstract Data Type. Manfred Broy and Martin Wirsing (Eds.)","author":"Ehrig Hartmut","year":"1983","unstructured":"Hartmut Ehrig, Werner Fey, and Horst Hansen. 1983. ACT ONE - an algebraic specification language with two levels of semantics. In Proceedings of the 2nd Workshop on Abstract Data Type. Manfred Broy and Martin Wirsing (Eds.), University of Passau, Department of Computer Science, Germany, 1 \u2013 ff."},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82534-4"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"e_1_3_3_46_2","volume-title":"Proceedings of the 4th Workshop on Automated deduction(Academic Press). W. H. Joyner (Ed.)","author":"Fay Michael Joseph","year":"1979","unstructured":"Michael Joseph Fay. 1979. First-order unification in an equational theory. In Proceedings of the 4th Workshop on Automated deduction(Academic Press). W. H. Joyner (Ed.), University of California, Santa Cruz, California, 161\u2013167."},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_36"},{"key":"e_1_3_3_49_2","doi-asserted-by":"publisher","unstructured":"Kokichi Futatsugi. 2015. Generate and check method for verifying transition systems in CafeOBJ. In Proceedings of the Software Services and Systems - Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering. Rocco De Nicola and Rolf Hennicker (Eds.) Lecture Notes in Computer Science Vol. 8950 Springer Berlin 171\u2013192. DOI:10.1007\/978-3-319-15545-6_13","DOI":"10.1007\/978-3-319-15545-6_13"},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2022.102893"},{"key":"e_1_3_3_51_2","volume-title":"CafeOBJ Report. World Scientific","author":"Futatsugi Kokichi","unstructured":"Kokichi Futatsugi and Razvan Diaconescu. 1998. CafeOBJ Report. World Scientific, Singapore."},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2012.07.041"},{"key":"e_1_3_3_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/318593.318610"},{"key":"e_1_3_3_54_2","volume-title":"Proceedings of the 8th IFIP Congress 1980","author":"Futatsugi Kokichi","year":"1980","unstructured":"Kokichi Futatsugi and Koji Okada. 1980. Specification writing as construction of hierarchically structured clusters of operators. In Information Processing, Proceedings of the 8th IFIP Congress 1980, Tokyo, Japan - October 6-9, 1980 and Melbourne, Australia - October 14-17, 1980. Simon H. Lavington (Ed.), North-Holland\/IFIP, Amsterdam, 287\u2013292."},{"key":"e_1_3_3_55_2","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC.2018.00024"},{"key":"e_1_3_3_56_2","doi-asserted-by":"publisher","DOI":"10.3217\/jucs-018-16-2204"},{"key":"e_1_3_3_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40206-7_26"},{"key":"e_1_3_3_58_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.393.8"},{"key":"e_1_3_3_59_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-51081-8_105"},{"key":"e_1_3_3_60_2","first-page":"307","article-title":"Completeness of many-sorted equational logic","volume":"11","author":"Goguen Joseph","year":"1985","unstructured":"Joseph Goguen and Jose Meseguer. 1985. Completeness of many-sorted equational logic. Houston Journal of Mathematics 11, 3 (1985), 307\u2013334.","journal-title":"Houston Journal of Mathematics"},{"key":"e_1_3_3_62_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1984.5010277"},{"key":"e_1_3_3_63_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-53162-9_27"},{"key":"e_1_3_3_64_2","doi-asserted-by":"publisher","DOI":"10.1142\/9789812794499_0004"},{"key":"e_1_3_3_65_2","unstructured":"Joseph A. Goguen. 1997. Tossing Algebraic Flowers Down the Great Divide. (1997). Retrieved from http:\/\/cseweb.ucsd.edu\/goguen\/pps\/tcs97.pdf"},{"key":"e_1_3_3_66_2","unstructured":"Joseph A. Goguen. 2021. Theorem proving and algebra. arXiv:2101.02690. Retrieved from https:\/\/arxiv.org\/abs\/2101.02690"},{"key":"e_1_3_3_67_2","doi-asserted-by":"publisher","DOI":"10.1145\/147508.147524"},{"key":"e_1_3_3_68_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-19242-5_22"},{"key":"e_1_3_3_69_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00275-3"},{"key":"e_1_3_3_70_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90302-V"},{"key":"e_1_3_3_71_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-6541-0_1"},{"key":"e_1_3_3_72_2","first-page":"1382","article-title":"Formal proof\u2013the four-color theorem","volume":"55","author":"Gonthier Georges","year":"2008","unstructured":"Georges Gonthier. 2008. Formal proof\u2013the four-color theorem. Notices of the AMS 55, 11 (2008), 1382\u20131393. Retrieved from https:\/\/www.ams.org\/notices\/200811\/tx081101382p.pdf","journal-title":"Notices of the AMS"},{"key":"e_1_3_3_73_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2020.09.024"},{"key":"e_1_3_3_74_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2704-5"},{"key":"e_1_3_3_75_2","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC.2017.75"},{"key":"e_1_3_3_76_2","doi-asserted-by":"publisher","DOI":"10.1017\/fmp.2017.1"},{"key":"e_1_3_3_77_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.359.16"},{"key":"e_1_3_3_78_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.393.13"},{"key":"e_1_3_3_79_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0031814"},{"key":"e_1_3_3_80_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008712907154"},{"key":"e_1_3_3_81_2","doi-asserted-by":"publisher","DOI":"10.1145\/3594735"},{"key":"e_1_3_3_82_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_3_83_2","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(85)90074-8"},{"key":"e_1_3_3_84_2","volume-title":"Retrieved","author":"HOL.","year":"2024","unstructured":"Isabelle\/HOL. 2024a. Isar. Retrieved January 15, 2024 from https:\/\/isabelle.in.tum.de\/Isar\/. (2024)."},{"key":"e_1_3_3_85_2","volume-title":"Retrieved","author":"HOL.","year":"2024","unstructured":"Isabelle\/HOL. 2024b. Sledgehammer. Retrieved January 15, 2024 from https:\/\/isabelle.in.tum.de\/website-Isabelle2009-1\/sledgehammer.html. (2024)."},{"key":"e_1_3_3_86_2","doi-asserted-by":"publisher","DOI":"10.1007\/11542384_16"},{"key":"e_1_3_3_87_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622827"},{"key":"e_1_3_3_88_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_3_89_2","doi-asserted-by":"publisher","DOI":"10.5555\/555902"},{"key":"e_1_3_3_90_2","volume-title":"Volumes 1-4B","author":"Knuth Donald E.","unstructured":"Donald E. Knuth. 2022. The Art of Computer Programming, Volumes 1-4B. Addison-Wesley, Boston, American."},{"key":"e_1_3_3_91_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.375.5"},{"key":"e_1_3_3_92_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-98938-9_16"},{"key":"e_1_3_3_93_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"e_1_3_3_94_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.393.10"},{"key":"e_1_3_3_95_2","doi-asserted-by":"publisher","unstructured":"K. Rustan M. Leino. 2010. Dafny: An automatic program verifier for functional correctness. In Logic for Programming Artificial Intelligence and Reasoning - 16th International Conference LPAR-16 Dakar Senegal April 25-May 1 2010 Revised Selected Papers. Edmund M. Clarke and Andrei Voronkov (Eds.) Lecture Notes in Computer Science Vol. 6355 Springer Berlin 348\u2013370. DOI:10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_3_96_2","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_3_98_2","doi-asserted-by":"publisher","DOI":"10.1145\/800055.802036"},{"key":"e_1_3_3_99_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-63790-2_25"},{"key":"e_1_3_3_100_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-024-00748-Z"},{"key":"e_1_3_3_101_2","volume-title":"Proceedings of the Handbook of Philosophical Logic","author":"Mart\u00ed-Oliet Narciso","unstructured":"Narciso Mart\u00ed-Oliet and Jos\u00e9 Meseguer. 2002. Rewriting logic as a logical and semantic framework. In Proceedings of the Handbook of Philosophical Logic, Second Edition, Volume 9. D. M. Gabbay and F. Guenthner (Eds.), Kluwer Academic Publishers, Dordrecht, The Netherlands, 1\u201387. First published as SRI Technical Report SRI-CSL-93-05, August 1993."},{"key":"e_1_3_3_102_2","volume-title":"Proceedings of the 5th International Workshop on Rewriting Logic and its Applications, WRLA 2004","author":"Meseguer Jos\u00e9","year":"2004","unstructured":"Jos\u00e9 Meseguer and Prasanna Thati. 2004. Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. In Proceedings of the 5th International Workshop on Rewriting Logic and its Applications, WRLA 2004, Barcelona, Spain, March 27 \u2013 April 4, 2004(Electronic Notes in Theoretical Computer Science), Narciso Mart\u00ed-Oliet (Ed.), Elsevier, Essex, UK, 147\u2013174."},{"key":"e_1_3_3_103_2","doi-asserted-by":"publisher","DOI":"10.1145\/3473571"},{"key":"e_1_3_3_104_2","doi-asserted-by":"publisher","DOI":"10.1109\/12.713311"},{"key":"e_1_3_3_105_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_40"},{"key":"e_1_3_3_106_2","unstructured":"Masaki Nakamura Kazutoshi Sakakibara and Kazuhiro Ogata. 2020. Specification description and verification of multitask hybrid systems in the OTS\/CafeOBJ method. arXiv:2010.15280. Retrieved from https:\/\/arxiv.org\/abs\/2010.15280"},{"key":"e_1_3_3_107_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ITP.2023.24"},{"key":"e_1_3_3_108_2","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575685"},{"key":"e_1_3_3_109_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_3_110_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39958-2_12"},{"key":"e_1_3_3_111_2","doi-asserted-by":"publisher","DOI":"10.1007\/11780274_31"},{"key":"e_1_3_3_112_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.02.018"},{"key":"e_1_3_3_113_2","doi-asserted-by":"publisher","unstructured":"Kazuhiro Ogata Daigo Yamagishi Takahiro Seino and Kokichi Futatsugi. 2004. Modeling and verification of hybrid systems based on equations. In Proceedings of the Design Methods and Applications for Distributed Embedded Systems IFIP 18th World Computer Congress TC10 Working Conference on Distributed and Parallel Embedded Systems DIPES 2004(IFIP). Bernd Kleinjohann Guang R. Gao Hermann Kopetz Lisa Kleinjohann and Achim Rettberg (Eds.) Vol. 150 Kluwer\/Springer Berlin 43\u201352. DOI:10.1007\/1-4020-8149-9_5","DOI":"10.1007\/1-4020-8149-9_5"},{"key":"e_1_3_3_114_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55602-8_217"},{"key":"e_1_3_3_115_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.192.6"},{"key":"e_1_3_3_116_2","doi-asserted-by":"publisher","DOI":"10.1145\/3208951"},{"key":"e_1_3_3_117_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.JSS.2022.111302"},{"key":"e_1_3_3_118_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-016-0398-7"},{"key":"e_1_3_3_119_2","volume-title":"Scores: A Survey\u201d.","author":"Riesco A.","year":"2024","unstructured":"A. Riesco, K. Ogata, M. Nakamura, D. G\u0103in\u0103, D. Dinh Tran, and K. Futatsugi. 2024. Supplemental materials for \u201cProof Scores: A Survey\u201d. (2024)."},{"key":"e_1_3_3_120_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54624-2_30"},{"key":"e_1_3_3_121_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2016.10.001"},{"key":"e_1_3_3_122_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.JLAMP.2024.101005"},{"key":"e_1_3_3_123_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-87181-9"},{"key":"e_1_3_3_124_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0027284"},{"key":"e_1_3_3_125_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90008-9"},{"key":"e_1_3_3_126_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17336-3"},{"key":"e_1_3_3_127_2","unstructured":"Toshimi Sawada Kokichi Futatsugi and Norbert Preining. 2018. CafeOBJ Reference Manual (version 1.5.7). JAIST."},{"key":"e_1_3_3_128_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29436-6_29"},{"key":"e_1_3_3_129_2","volume-title":"Proceedings of the 17th International Conference on Software Engineering and Knowledge Engineering","author":"Senachak Jittisak","year":"2005","unstructured":"Jittisak Senachak, Takahiro Seino, Kazuhiro Ogata, and Kokichi Futatsugi. 2005. Provably correct translation from CafeOBJ into java. In Proceedings of the 17th International Conference on Software Engineering and Knowledge Engineering, Taipei, Taiwan, Republic of China, July 14-16, 2005. William C. Chu, Natalia Juristo Juzgado, and W. Eric Wong (Eds.), KSI Research Inc. and Knowledge Systems Institute Graduate School, Pittsburgh, USA, 614\u2013619."},{"key":"e_1_3_3_130_2","doi-asserted-by":"publisher","DOI":"10.1142\/S0218126624501123"},{"key":"e_1_3_3_131_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"e_1_3_3_132_2","volume-title":"Term Rewriting Systems","unstructured":"Terese. 2003. Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, Vol. 55, Cambridge University Press, Cambridge, CB2 8BS, United Kingdom."},{"key":"e_1_3_3_133_2","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2021.3093211"},{"key":"e_1_3_3_134_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.cose.2022.102909"},{"key":"e_1_3_3_135_2","doi-asserted-by":"publisher","DOI":"10.1145\/3497775.3503689"},{"key":"e_1_3_3_136_2","first-page":"373","article-title":"Algebraic specifications: Some old history and new thoughts","volume":"9","author":"Wagner Eric G.","year":"2002","unstructured":"Eric G. Wagner. 2002. Algebraic specifications: Some old history and new thoughts. Nordic Journal of Computing 9, 4 (2002), 373\u2013404.","journal-title":"Nordic Journal of Computing"},{"key":"e_1_3_3_137_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-6164-6"},{"key":"e_1_3_3_138_2","volume-title":"Woodcock and Jim Davies","author":"J. C.","year":"1996","unstructured":"J. C. P. Woodcock and Jim Davies. 1996. Using Z - Specification, Refinement, and Proof. Prentice Hall, New Jersey, USA."},{"key":"e_1_3_3_139_2","doi-asserted-by":"publisher","DOI":"10.1145\/3609437.3609460"},{"key":"e_1_3_3_140_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-024-09709-2"},{"key":"e_1_3_3_141_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498677"}],"container-title":["ACM Computing Surveys"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729166","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729166","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:18:48Z","timestamp":1750295928000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729166"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,7]]},"references-count":137,"journal-issue":{"issue":"10","published-print":{"date-parts":[[2025,10,31]]}},"alternative-id":["10.1145\/3729166"],"URL":"https:\/\/doi.org\/10.1145\/3729166","relation":{},"ISSN":["0360-0300","1557-7341"],"issn-type":[{"value":"0360-0300","type":"print"},{"value":"1557-7341","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,5,7]]},"assertion":[{"value":"2024-02-29","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-01","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-05-07","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}