{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T19:00:37Z","timestamp":1757617237193,"version":"3.44.0"},"reference-count":93,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2025,1,8]],"date-time":"2025-01-08T00:00:00Z","timestamp":1736294400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,1,8]],"date-time":"2025-01-08T00:00:00Z","timestamp":1736294400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100003246","name":"Nederlandse Organisatie voor Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","award":["VICI 639.023.710"],"award-info":[{"award-number":["VICI 639.023.710"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2025,8]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>In software engineering, models are used for many different things. In this paper, we focus on program verification, where we use models to reason about the correctness of systems. There are many different types of program verification techniques which provide different correctness guarantees. We investigate the domain of program verification tools and present a concise megamodel to distinguish these tools. We also present a data set of 400+ program verification tools. This data set includes the category of verification tool according to our megamodel, practical information such as input\/output format, repository links and more. The practical information, such as last commit date, is kept up to date through the use of APIs.  Moreover, part of the data extraction has been automated to make it easier to expand the data set. The categorisation enables software engineers to find suitable tools, investigate alternatives and compare tools. We also identify trends for each level in our megamodel. Our data set, publicly available at <jats:ext-link xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" xlink:href=\"https:\/\/doi.org\/10.4121\/20347950\" ext-link-type=\"uri\">https:\/\/doi.org\/10.4121\/20347950<\/jats:ext-link>, can be used by software engineers to enter the world of program verification and find a verification tool based on their requirements. This paper is an extended version of <jats:ext-link xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" xlink:href=\"https:\/\/doi.org\/10.1145\/3550355.3552426\" ext-link-type=\"uri\">https:\/\/doi.org\/10.1145\/3550355.3552426<\/jats:ext-link>.<\/jats:p>","DOI":"10.1007\/s10270-024-01232-7","type":"journal-article","created":{"date-parts":[[2025,1,8]],"date-time":"2025-01-08T00:48:26Z","timestamp":1736297306000},"page":"1293-1313","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Extract, model, refine: improved modelling of program verification tools through data enrichment"],"prefix":"10.1007","volume":"24","author":[{"given":"Sophie","family":"Lathouwers","sequence":"first","affiliation":[]},{"given":"Yujie","family":"Liu","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7764-4224","authenticated-orcid":false,"given":"Vadim","family":"Zaytsev","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,1,8]]},"reference":[{"key":"1232_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Chen, Y.-F., Clemente, L., Hol\u00edk, L., Hong, C.-D., Mayr, R., Vojnar, T.: Simulation subsumption in Ramsey-based B\u00fcchi automata universality and inclusion testing. In: Touili, T., Cook, B., Jackson, P. (Eds.), In: Proceedings of the 22nd international conference on computer aided verification (CAV) (pp. 132\u2013147). Springer (2010)","DOI":"10.1007\/978-3-642-14295-6_14"},{"key":"1232_CR2","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A., D\u2019Antoni, L., Drews, S.: Repairing decision-making programs under uncertainty. In: Majumdar, R., Kun\u010dak, V. (Eds.), In: Proceedings of the 29th international conference on computer aided verification (CAV) (pp. 181\u2013200). Springer (2017)","DOI":"10.1007\/978-3-319-63387-9_9"},{"key":"1232_CR3","doi-asserted-by":"crossref","unstructured":"Alsmadi, I., Alazzam, I.: Software attributes that impact popularity. In: Proceedings of the eighth international conference on information technology (ICIT) (pp. 205\u2013208) (2017)","DOI":"10.1109\/ICITECH.2017.8080001"},{"key":"1232_CR4","doi-asserted-by":"crossref","unstructured":"Amy, M., Roetteler, M., Svore, K.M.: Verified compilation of space-efficient reversible circuits. Majumdar, R., Kun\u010dak, V. (Eds.), In: Proceedings of the 28th international conference on computer aided verification (CAV) (pp. 3\u201321). Springer (2017)","DOI":"10.1007\/978-3-319-63390-9_1"},{"key":"1232_CR5","doi-asserted-by":"crossref","unstructured":"Andova, S., van\u00a0den Brand, M., Engelen, L.J.P., Verhoeff, T.: MDE basics with a DSL focus. In: Advanced lectures of the 12th international school on formal methods for the design of computer, communication and software systems: formal methods for model-driven engineering (Vol. 7320, pp. 21\u201357). Springer (2012)","DOI":"10.1007\/978-3-642-30982-3_2"},{"key":"1232_CR6","doi-asserted-by":"crossref","unstructured":"Arndt, H., Jansen, C., Katoen, J.-P., Matheja, C., Noll, T.: Let this graph be your witness! In: Chockler, H., Weissenbacher, G. (Eds.), In: Proceedings of the 30th international conference on computer aided verification (CAV) (pp. 3\u201311). Springer (2018)","DOI":"10.1007\/978-3-319-96142-2_1"},{"key":"1232_CR7","unstructured":"Ashok, P., Jackermeier, M., K\u0159et\u00ednsk\u00fd, J., Weinhuber, C., Weininger, M., Yadav, M.: dtControl 2.0: explainable strategy representation via decision tree learning steered by experts. In: Groote, J.F., Larsen, K.G. (eds.) In: International conference on tools and algorithms for the construction and analysis of systems, pp. 326\u2013345. Springer, Cham (2021)"},{"key":"1232_CR8","doi-asserted-by":"crossref","unstructured":"Aydemir, B.E., Bohannon, A., Fairbairn, M., Foster, J.N., Pierce, B.C., Sewell, P., Zdancewic, S.: Mechanized metatheory for the masses: the PoplMark challenge. In: Hurd, J., Melham, T.F. (Eds.), In: Proceedings of the 18th international conference on theorem proving in higher order logics (TPHOLs) (Vol. 3603, pp. 50\u201365). Springer (2005)","DOI":"10.1007\/11541868_4"},{"key":"1232_CR9","doi-asserted-by":"crossref","unstructured":"Baier, C., Coenen, N., Finkbeiner, B., Funke, F., Jantsch, S., Siber, J.: Causality-based game solving. In: Silva, A., Leino, K.R.M. (eds.) In: International conference on computer aided verification, pp. 894\u2013917. Springer, Cham (2021)","DOI":"10.1007\/978-3-030-81685-8_42"},{"issue":"2","key":"1232_CR10","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1145\/3554976","volume":"66","author":"MT Baldassarre","year":"2023","unstructured":"Baldassarre, M.T., Ernst, N., Hermann, B., Menzies, T., Yedida, R.: (Re) use of research results (is rampant). Commun. ACM 66(2), 75\u201381 (2023). https:\/\/doi.org\/10.1145\/3554976","journal-title":"Commun. ACM"},{"key":"1232_CR11","doi-asserted-by":"publisher","unstructured":"Barbon, G., Leroy, V., Sala\u00fcn, G.: Debugging of behavioural models with CLEAR. In: Vojnar, T., Zhang, L. (eds.) Tools and algorithms for the construction and analysis of systems: 25th International Conference, TACAS 2019 pp. 386\u2013392. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_26","DOI":"10.1007\/978-3-030-17462-0_26"},{"key":"1232_CR12","doi-asserted-by":"crossref","unstructured":"Barringer, H., Havelund, K.: TraceContract: a Scala DSL for trace analysis. In: Proceedings of the 17th international symposium of formal methods (Vol. 6664, pp. 57\u201372). Springer (2011)","DOI":"10.1007\/978-3-642-21437-0_7"},{"key":"1232_CR13","doi-asserted-by":"crossref","unstructured":"Bauer, M.S., Chadha, R., Prasad Sistla, A.R., Viswanathan, M.: Model checking indistinguishability of randomized security protocols. In: Chockler, H., Weissenbacher, G. (eds.) In: International conference on computer aided verification (CAV), pp. 117\u2013135. Springer, Cham (2018)","DOI":"10.1007\/978-3-319-96142-2_10"},{"key":"1232_CR14","first-page":"232","volume-title":"Hybrid systems","author":"J Bengtsson","year":"1996","unstructured":"Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL: a tool suite for automatic verification of real-time systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) Hybrid systems, pp. 232\u2013243. Springer, Cham (1996)"},{"key":"1232_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive theorem proving and program development: Coq\u2019art: the calculus of inductive constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive theorem proving and program development: Coq\u2019art: the calculus of inductive constructions. Springer, London (2004)"},{"key":"1232_CR16","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-030-99527-0_20","volume-title":"Tools and algorithms for the construction and analysis of systems","author":"D Beyer","year":"2022","unstructured":"Beyer, D.: Progress on software verification: Sv-comp 2022. In: Fisman, D., Rosu, G. (eds.) Tools and algorithms for the construction and analysis of systems, pp. 375\u2013402. Springer, Cham (2022)"},{"key":"1232_CR17","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer aided verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: Cpachecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer aided verification, pp. 184\u2013190. Springer, Cham (2011)"},{"issue":"2","key":"1232_CR18","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s00165-005-0079-4","volume":"18","author":"J Bicarregui","year":"2006","unstructured":"Bicarregui, J., Hoare, C.A.R., Woodcock, J.C.P.: The verified software repository: a step towards the verifying compiler. Formal Asp. Comput. 18(2), 143\u2013151 (2006). https:\/\/doi.org\/10.1007\/s00165-005-0079-4","journal-title":"Formal Asp. Comput."},{"key":"1232_CR19","doi-asserted-by":"crossref","unstructured":"Bodeveix, J., Filali, M., Lawall, J., Muller, G.: Formal methods meet domain specific languages. In: Romijn, J., Smith, G., van de Pol, J. (Eds.), In: Proceedings of the fifth international conference on integrated formal methods (IFM) (Vol. 3771, pp. 187\u2013206). Springer (2005)","DOI":"10.1007\/11589976_12"},{"key":"1232_CR20","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-662-54577-5_6","volume-title":"Tools and algorithms for the construction and analysis of systems","author":"C Borralleras","year":"2017","unstructured":"Borralleras, C., Brockschmidt, M., Larraz, D., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Proving termination through conditional termination. In: Legay, A., Margaria, T. (eds.) Tools and algorithms for the construction and analysis of systems, pp. 99\u2013117. Springer, Cham (2017)"},{"key":"1232_CR21","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/978-3-319-63387-9_21","volume-title":"Computer aided verification","author":"T Brihaye","year":"2017","unstructured":"Brihaye, T., Geeraerts, G., Ho, H.M., Monmege, B.: Mightyl: a compositional translation from MITL to timed automata. In: Majumdar, R., Kun\u010dak, V. (eds.) Computer aided verification, pp. 421\u2013440. Springer, Cham (2017)"},{"key":"1232_CR22","doi-asserted-by":"crossref","unstructured":"Broadfoot, G.H., Broadfoot, P.J.: Academia and industry meet: some experiences of formal methods in practice. Proceedings of the 10th asia-pacific software engineering conference (APSEC) (p.49). IEEE Computer Society (2003)","DOI":"10.1109\/APSEC.2003.1254357"},{"key":"1232_CR23","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1109\/MS.2020.3041522","volume":"38","author":"A Bucchiarone","year":"2021","unstructured":"Bucchiarone, A., Ciccozzi, F., Lambers, L., Pierantonio, A., Tichy, M., Tisi, M., Zaytsev, V.: What is the future of modelling? IEEE Softw. Insights (IEEE Softw.) 38, 119\u2013127 (2021). https:\/\/doi.org\/10.1109\/MS.2020.3041522","journal-title":"IEEE Softw. Insights (IEEE Softw.)"},{"key":"1232_CR24","doi-asserted-by":"crossref","unstructured":"Canet, G., Cuoq, P., Monate, B.: A value analysis for C programs. In: Ninth IEEE international working conference on source code analysis and manipulation, SCAM 2009, 2009 (pp. 123\u2013124). IEEE Computer Society (2009)","DOI":"10.1109\/SCAM.2009.22"},{"key":"1232_CR25","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-662-49674-9_17","volume-title":"Tools and algorithms for the construction and analysis of systems","author":"Z Chen","year":"2016","unstructured":"Chen, Z., Wang, Z., Zhu, Y., Xi, H., Yang, Z.: Parametric runtime verification of C programs. In: Chechik, M., Raskin, J.F. (eds.) Tools and algorithms for the construction and analysis of systems, pp. 299\u2013315. Springer, Cham (2016)"},{"issue":"2","key":"1232_CR26","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1016\/j.joi.2017.03.003","volume":"11","author":"EA Corr\u00eaa Jr","year":"2017","unstructured":"Corr\u00eaa, E.A., Jr., Silva, F.N., da F. Costa, L., Amancio, D.R.: Patterns of authors contribution in scientific manuscripts. J. Inform. 11(2), 498\u2013510 (2017). https:\/\/doi.org\/10.1016\/j.joi.2017.03.003","journal-title":"J. Inform."},{"issue":"1","key":"1232_CR27","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/s10270-022-01010-3","volume":"22","author":"I David","year":"2023","unstructured":"David, I., Latifaj, M., Pietron, J., Zhang, W., Ciccozzi, F., Malavolta, I., Hebig, R.: Blended modeling in commercial and open-source model-driven software engineering tools: a systematic study. Softw. Syst. Model. 22(1), 415\u2013447 (2023). https:\/\/doi.org\/10.1007\/s10270-022-01010-3","journal-title":"Softw. Syst. Model."},{"key":"1232_CR28","doi-asserted-by":"crossref","unstructured":"Davis, J.A., Clark, M.A., Cofer, D.D., Fifarek, A., Hinchman, J., Hoffman, J.A., Wagner, L.G.: Study on the barriers to the industrial adoption of formal methods. In: Pecheur, C., Dierkes, M. (Eds.), In: Proceedings of the 18th international workshop on formal methods for industrial critical systems (FMICS) (Vol. 8187, pp. 63\u201377). Springer (2013)","DOI":"10.1007\/978-3-642-41010-9_5"},{"key":"1232_CR29","doi-asserted-by":"crossref","unstructured":"de Moura, L., Ullrich, S.: The lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, A. (Eds.), In: Proceedings of the 28th International conference on automated deduction (CADE) (pp. 625\u2013635). Springer (2021)","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"1232_CR30","doi-asserted-by":"crossref","unstructured":"de Moura, L.M., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (Eds.), In: Proceedings of the 14th international conference on tools and algorithms for the construction and analysis of systems (tacas) (Vol. 4963, pp. 337\u2013340). Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"1232_CR31","doi-asserted-by":"crossref","unstructured":"Djoudi, A., Bardin, S.: BINSEC: binary code analysis with low-level regions. In: Baier, C., Tinelli, C. (Eds.), In: Proceedings of the 21st international conference on tools and algorithms for the construction and analysis of systems (TACAS) (Vol. 9035, pp. 212\u2013217). Springer (2015)","DOI":"10.1007\/978-3-662-46681-0_17"},{"key":"1232_CR32","doi-asserted-by":"crossref","unstructured":"Dohrau, J., Summers, A.J., Urban, C., M\u00fcnger, S., M\u00fcller, P.: Permission inference for array programs. In: Chockler, H., Weissenbacher, G. (eds) In: Computer aided verification. CAV 2018. (pp. 55\u201374). Springer (2018)","DOI":"10.1007\/978-3-319-96142-2_7"},{"key":"1232_CR33","doi-asserted-by":"crossref","unstructured":"Drews, S., Albarghouthi, A., D\u2019Antoni, L.: Efficient synthesis with probabilistic constraints. In: Dillig, I., Tasiran, S. (Eds.), Proceedings of the 30th international conference on computer aided verification (CAV) (pp. 278\u2013296). Springer (2019)","DOI":"10.1007\/978-3-030-25540-4_15"},{"key":"1232_CR34","doi-asserted-by":"crossref","unstructured":"Ernst, G., Murray, T.: SecCSL: Security concurrent separation logic. In: Dillig, I., Tasiran, S. (Eds.), In: Computer aided verification: 31st international conference, CAV 2019 (pp. 208\u2013230). Springer (2019)","DOI":"10.1007\/978-3-030-25543-5_13"},{"key":"1232_CR35","doi-asserted-by":"crossref","unstructured":"Evrard, H.: Dlc: Compiling a concurrent system formal specification to a distributed implementation. In: Chechik, M., Raskin JF (Eds.), In: Tools and algorithms for the construction and analysis of systems: 22nd international conference, TACAS 2016 (pp. 553\u2013559). Springer (2016)","DOI":"10.1007\/978-3-662-49674-9_34"},{"issue":"2","key":"1232_CR36","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/s10009-021-00609-z","volume":"23","author":"Y Falcone","year":"2021","unstructured":"Falcone, Y., Krstic, S., Reger, G., Traytel, D.: A taxonomy for classifying runtime verification tools. Int. J. Softw. Tools Technol. Transf. 23(2), 255\u2013284 (2021). https:\/\/doi.org\/10.1007\/s10009-021-00609-z","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1232_CR37","doi-asserted-by":"crossref","unstructured":"Ferrari, A., Mazzanti, F., Basile, D., Beek, M.H.t., Fantechi, A.: Comparing formal tools for system design: a judgment study. In: Proceedings of the ACM\/IEEE 42nd international conference on software engineering (pp. 62\u201374). Association for Computing Machinery (2020)","DOI":"10.1145\/3377811.3380373"},{"key":"1232_CR38","doi-asserted-by":"crossref","unstructured":"Foley, M.J., Kochalko, D.L.: Open researcher and contributor identifier, a contemporary Stanley. (2012) https:\/\/docs.lib.purdue.edu\/cgi\/viewcontent.cgi?article=1133&context=charleston","DOI":"10.5703\/1288284314850"},{"key":"1232_CR39","unstructured":"Fowler, M.: Language workbenches: the killer-app for domain specific languages? MartinFowler.com. https:\/\/martinfowler.com\/articles\/languageWorkbench.html"},{"key":"1232_CR40","doi-asserted-by":"crossref","unstructured":"Frey, G., Litz, L.: Formal methods in PLC programming. In: Proceedings of the international conference on systems, man & cybernetics: \u201cCybernetics evolving to systems, humans, organizations, and their complex interactions\u201d (pp. 2431\u20132436). IEEE (2000)","DOI":"10.1109\/ICSMC.2000.884356"},{"key":"1232_CR41","doi-asserted-by":"crossref","unstructured":"Goldwasser, S., Micali, S., Rackoff, C.: The knowledge complexity of interactive proof-systems. In: Proceedings of the seventeenth annual ACM symposium on theory of computing (SToC) (p. 291\u2013304). Association for Computing Machinery (1985)","DOI":"10.1145\/22145.22178"},{"key":"1232_CR42","doi-asserted-by":"crossref","unstructured":"Gopinathan, K., Sergey, I.: Certifying certainty and uncertainty in approximate membership query structures. In: Lahiri, S.K., Wang, C. (Eds.), In: Computer aided verification: 32nd international conference, CAV 2020 (CAV) (pp. 279\u2013303). Springer (2020)","DOI":"10.1007\/978-3-030-53291-8_16"},{"key":"1232_CR43","doi-asserted-by":"crossref","unstructured":"Guo, X., Lesourd, M., Liu, M., Rieg, L., Shao, Z.: Integrating formal schedulability analysis into a verified OS kernel. In: Dillig, I., Tasiran, S. (Eds.), In: Computer aided verification: 31st international conference, CAV 2019 (pp. 496\u2013514). Springer (2019)","DOI":"10.1007\/978-3-030-25543-5_28"},{"key":"1232_CR44","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantitative verification benchmark set. In: Vojnar, T., Zhang, L. (Eds.), In: Proceedings of the 25th international conference on tools and algorithms for the construction and analysis of systems (TACAS) (Vol. 11427, pp. 344\u2013350). Springer (2019)","DOI":"10.1007\/978-3-030-17462-0_20"},{"key":"1232_CR45","unstructured":"Harz, D., Knottenbelt, W.J.: Towards safer smart contracts: a survey of languages and verification methods. CoRR, (2018) arxiv:1809.09805"},{"key":"1232_CR46","doi-asserted-by":"crossref","unstructured":"Hassan, M., Urban, C., Eilers, M., M\u00fcller, P.: Maxsmt-based type inference for Python 3. In: Chockler, H., Weissenbacher, G. (Eds.), In: Computer aided verification: 30th international conference, CAV 2018, (pp. 12\u201319). Springer (2018)","DOI":"10.1007\/978-3-319-96142-2_2"},{"key":"1232_CR47","doi-asserted-by":"crossref","unstructured":"Hermann, B., Winter, S., Siegmund, J.: Community expectations for research artifacts and evaluation processes. In: Proceedings of the 28th ACM joint meeting on European software engineering conference and symposium on the foundations of software engineering (p. 469\u2013480). New York, NY, USA: Association for Computing Machinery (2020)","DOI":"10.1145\/3368089.3409767"},{"key":"1232_CR48","doi-asserted-by":"crossref","unstructured":"Hol\u00edk, L., Hru\u0161ka, M., Leng\u00e1l, O., Rogalewicz, A., \u0160im\u00e1\u010dek, J., Vojnar, T.: Forester: from heap shapes to automata predicates. In: Legay, A., Margaria, T. (Eds.), In: Proceedings of tools and algorithms for the construction and analysis of systems (pp. 365\u2013369). Springer (2017)","DOI":"10.1007\/978-3-662-54580-5_24"},{"key":"1232_CR49","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1016\/j.scico.2013.03.017","volume":"89","author":"JE Hutchinson","year":"2014","unstructured":"Hutchinson, J.E., Whittle, J., Rouncefield, M.: Model-driven engineering practices in industry: social, organizational and managerial factors that lead to success or failures. Sci. Comput. Progr. 89, 144\u2013161 (2014). https:\/\/doi.org\/10.1016\/j.scico.2013.03.017","journal-title":"Sci. Comput. Progr."},{"key":"1232_CR50","doi-asserted-by":"publisher","unstructured":"Jin, P., Tian, J., Zhi, D., Wen, X., Zhang, M.: Trainify: a CEGAR-driven training and verification framework for safe deep reinforcement learning. In: Shoham, S., Vizel, Y. (Eds.), In: International conference on computer aided verification (pp. 193\u2013218). Cham: Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_10","DOI":"10.1007\/978-3-031-13185-1_10"},{"key":"1232_CR51","doi-asserted-by":"crossref","unstructured":"Jongmans, S.-S.T.Q., Arbab, F.: Prdk: protocol programming with automata. In: Chechik, M., Raskin, J.F. (Eds.), In: Tools and algorithms for the construction and analysis of systems: 22nd international conference, TACAS 2016 (pp. 547\u2013552). Springer (2016)","DOI":"10.1007\/978-3-662-49674-9_33"},{"key":"1232_CR52","doi-asserted-by":"crossref","unstructured":"Kl\u00f6sch, R., Eixelsberger, W.: Challenges and experiences in managing major software evolution endeavours such as euro conversion or Y2000 compliance. In: Proceedings of the 15th international conference on software maintenance (ICSM) (pp. 161\u2013166). IEEE Computer Society (1999)","DOI":"10.1109\/ICSM.1999.792600"},{"key":"1232_CR53","doi-asserted-by":"crossref","unstructured":"K\u00f6lbl, M., Leue, S., Wies, T.: Tartar: a timed automata repair tool. In: Lahiri, S.K., Wang, C. (Eds.), In: Computer aided verification: 32nd international conference, CAV 2020 (pp. 529\u2013540). Springer (2020)","DOI":"10.1007\/978-3-030-53288-8_25"},{"key":"1232_CR54","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., & Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (Eds.), In: International conference on computer aided verification (pp. 1\u201335). Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_1"},{"issue":"3","key":"1232_CR55","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/2464526.2464530","volume":"38","author":"S Krishnamurthi","year":"2013","unstructured":"Krishnamurthi, S.: Artifact evaluation for software conferences. ACM SIGSOFT Softw. Eng. Notes 38(3), 7\u201310 (2013)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"1232_CR56","doi-asserted-by":"crossref","unstructured":"Kula, R.G., De\u00a0Roover, C., German, D.M., Ishio, T., Inoue, K.: A generalized model for visualizing library popularity, adoption, and diffusion within a software ecosystem. In: Proceedings of the 25th IEEE international conference on software analysis, evolution and reengineering (SANER) (pp. 288\u2013299) (2018)","DOI":"10.1109\/SANER.2018.8330217"},{"issue":"3","key":"1232_CR57","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Trans. Progr. Lang. Syst. (ToPLaS) 16(3), 872\u2013923 (1994). https:\/\/doi.org\/10.1145\/177492.177726","journal-title":"ACM Trans. Progr. Lang. Syst. (ToPLaS)"},{"key":"1232_CR58","doi-asserted-by":"publisher","unstructured":"Lathouwers, S., Zaytsev, V.: Modelling program verification tools for software engineers. In: Proceedings of the 25th international conference on model driven engineering languages and systems (p.98-108). New York, NY, USA: Association for Computing Machinery (2022) https:\/\/doi.org\/10.1145\/3550355.3552426","DOI":"10.1145\/3550355.3552426"},{"key":"1232_CR59","doi-asserted-by":"crossref","unstructured":"Li, J., Vardi, M.Y., Rozier, K.Y.: Satisfiability checking for mission-time LTL. In: Dillig, I., Tasiran, S. (Eds.), In: Computer aided verification: 31st international conference, CAV 2019 (pp. 3\u201322). Springer (2019)","DOI":"10.1007\/978-3-030-25543-5_1"},{"key":"1232_CR60","doi-asserted-by":"crossref","unstructured":"Mann, M., Wilson, A., Zohar, Y., Stuntz, L., Irfan, A., Brown, K., Barrett, C.W.: Smt-switch: a solver-agnostic C++ API for SMT solving. In: Li, C., Many\u00e0, F. (Eds.), In: International conference on theory and applications of satisfiability testing (Vol. 12831, pp. 377\u2013386). Springer (2021)","DOI":"10.1007\/978-3-030-80223-3_26"},{"issue":"3","key":"1232_CR61","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10617-012-9096-8","volume":"16","author":"W Meeus","year":"2012","unstructured":"Meeus, W., Beeck, K.V., Goedem\u00e9, T., Meel, J., Stroobandt, D.: An overview of today\u2019s high-level synthesis tools. Des. Autom. Embed. Syst. 16(3), 31\u201351 (2012). https:\/\/doi.org\/10.1007\/s10617-012-9096-8","journal-title":"Des. Autom. Embed. Syst."},{"key":"1232_CR62","doi-asserted-by":"crossref","unstructured":"Mr\u00e1zek, J., Bauch, P., Lauko, H., Barnat, J.: Symdivine: tool for control-explicit data-symbolic state space exploration. In: Bo\u0161na\u010dki, D., Wijs, A. (Eds.), In: Model Checking Software: 23rd international symposium, SPIN 2016 (pp. 208\u2013213). Springer (2016)","DOI":"10.1007\/978-3-319-32582-8_14"},{"key":"1232_CR63","doi-asserted-by":"crossref","unstructured":"Neupane, T., Myers, C.J., Madsen, C., Zheng, H., Zhang, Z.: Stamina: stochastic approximate model-checker for infinite-state analysis. In: Dillig, I., Tasiran, S. (Eds.), In: Computer aided verification: 31st international conference, CAV 2019 (pp. 540\u2013549). Springer (2019)","DOI":"10.1007\/978-3-030-25540-4_31"},{"key":"1232_CR64","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Barrett, C.: Murxla: a modular and highly extensible API fuzzer for SMT solvers. In: Shoham, S., Vizel, Y. (Eds.), In: International conference on computer aided verification (pp. 92\u2013106). Cham: Springer (2022)r","DOI":"10.1007\/978-3-031-13188-2_5"},{"key":"1232_CR65","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: a proof assistant for higher-order logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL: a proof assistant for higher-order logic, pp. 67\u2013104. Springer, Cham (2002)"},{"key":"1232_CR66","doi-asserted-by":"crossref","unstructured":"Nurwidyantoro, A., Shahin, M., Chaudron, M., Hussain, W., Perera, H., Shams, R.A., Whittle, J.: Towards a human values dashboard for software development: an exploratory study. In: Lanubile, F., Kalinowski, M., Baldassarre, M.T. (Eds.), In: Proceedings of the 15th international symposium on empirical software engineering and measurement (esem) (pp. 23:1\u201323:12). ACM (2021)","DOI":"10.1145\/3475716.3475770"},{"key":"1232_CR67","doi-asserted-by":"publisher","first-page":"106731","DOI":"10.1016\/j.infsof.2021.106731","volume":"141","author":"A Nurwidyantoro","year":"2022","unstructured":"Nurwidyantoro, A., Shahin, M., Chaudron, M.R.V., Hussain, W., Shams, R.A., Perera, H., Whittle, J.: Human values in software development artefacts: a case study on issue discussions in three android applications. Info. Softw. Technol. 141, 106731 (2022). https:\/\/doi.org\/10.1016\/j.infsof.2021.106731","journal-title":"Info. Softw. Technol."},{"key":"1232_CR68","doi-asserted-by":"crossref","unstructured":"Ojamaa, A., Haav, H.-M., Penjam, J.: Semi-automated generation of DSL meta models from formal domain ontologies. In: Bellatreche, L., Manolopoulos, Y. (Eds.), In: Model and data engineering: 5th international conference, MEDI 2015 (pp. 3\u201315). Cham: Springer (2015)","DOI":"10.1007\/978-3-319-23781-7_1"},{"key":"1232_CR69","volume-title":"The definitive ANTLR 4 reference","author":"T Parr","year":"2013","unstructured":"Parr, T.: The definitive ANTLR 4 reference. Pragmatic Bookshelf, Raleigh (2013)"},{"key":"1232_CR70","doi-asserted-by":"crossref","unstructured":"Peyras, Q., Bodeveix, J.-P., Brunel, J., Chemouil, D.: Sound verification procedures for temporal properties of infinite-state systems. In: Silva, A., Leino, K.R.M. (Eds.), In: Computer aided verification: 33rd international conference, CAV 2021 (pp. 337\u2013360). Springer (2021)","DOI":"10.1007\/978-3-030-81688-9_16"},{"key":"1232_CR71","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th annual symposium on foundations of computer science (pp. 46\u201357). IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"1232_CR72","doi-asserted-by":"crossref","unstructured":"Punnoose, R.J., Armstrong, R.C., Wong, M.H., Jackson, M.: Survey of existing tools for formal verification. (Tech. Rep.). USDOE National Nuclear Security Administration (NNSA) (2014)","DOI":"10.2172\/1166644"},{"key":"1232_CR73","doi-asserted-by":"crossref","unstructured":"Richter, C., Wehrheim, H.: Pesco: predicting sequential combinations of verifiers. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (Eds.), In: Tools and algorithms for the construction and analysis of systems: 25 years of TACAS: TOOLympics (pp. 229\u2013233). Springer (2019)","DOI":"10.1007\/978-3-030-17502-3_19"},{"key":"1232_CR74","doi-asserted-by":"crossref","unstructured":"Rothenberg, B.-C., Grumberg, O.: Must fault localization for program repair. In: Lahiri, S.K., Wang, C. (Eds.), In: Computer aided verification: 32nd international conference, CAV 2020 (pp. 658\u2013680). Springer (2020)","DOI":"10.1007\/978-3-030-53291-8_33"},{"key":"1232_CR75","doi-asserted-by":"crossref","unstructured":"Ryou, W., Chen, J., Balunovic, M., Singh, G., Dan, A., Vechev, M.: Scalable polyhedral verification of recurrent neural networks. In: Silva, A., Leino, K.R.M. (Eds.), In: Computer aided verification: 33rd international conference, CAV 2021 (pp. 225\u2013248). Springer (2021)","DOI":"10.1007\/978-3-030-81685-8_10"},{"key":"1232_CR76","doi-asserted-by":"crossref","unstructured":"Sajnani, H., Saini, V., Ossher, J., Lopes, C.V.: Is popularity a measure of quality? an analysis of maven components. In: Proceedings of the 2014 IEEE International conference on software maintenance and evolution (pp. 231\u2013240) (2014)","DOI":"10.1109\/ICSME.2014.45"},{"key":"1232_CR77","doi-asserted-by":"crossref","unstructured":"Schlick, R., Felderer, M., Majzik, I., Nardone, R., Raschke, A., Snook, C.F., Vittorini, V.: A proposal of an example and experiments repository to foster industrial adoption of formal methods. In: Margaria, T., Steffen, B. (Eds.), In: Proceedings of the eighth international symposium on leveraging applications of formal methods, verification and validation (ISoLA) (Vol. LNCS 11247, pp. 249\u2013272). Springer (2018)","DOI":"10.1007\/978-3-030-03427-6_20"},{"key":"1232_CR78","doi-asserted-by":"crossref","unstructured":"Shaaban, A.M., Schmittner, C., Gruber, T., Mohamed, A.B., Quirchmayr, G., Schikuta, E.: Ontology-based model for automotive security verification and validation. In: Proceedings of the 21st international conference on information integration and web-based applications & services (IIWAS) (pp. 73\u201382). ACM (2019)","DOI":"10.1145\/3366030.3366070"},{"key":"1232_CR79","unstructured":"Shipil\u00ebv, A.: Java concurrency stress (jcstress). (2013) https:\/\/github.com\/openjdk\/jcstress\/"},{"key":"1232_CR80","doi-asserted-by":"crossref","unstructured":"Siavvas, M., Jankovic, M., Kehagias, D., Tzovaras, D.: Is popularity an indicator of software security? In: Proceedings if the international conference on intelligent systems (IS) (pp. 692\u2013697) (2018)","DOI":"10.1109\/IS.2018.8710484"},{"key":"1232_CR81","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-8327-4","volume-title":"Allgemeine modelltheorie","author":"H Stachowiak","year":"1973","unstructured":"Stachowiak, H.: Allgemeine modelltheorie. Springer, Cham (1973)"},{"key":"1232_CR82","doi-asserted-by":"crossref","unstructured":"Tomasco, E., Nguyen, T.L., Inverso, O., Fischer, B., La\u00a0Torre, S., Parlato, G.: Mu-cseq 0.4: individual memory location unwindings. In: Chechik, M., Raskin, J.-F., (Eds.), In: Tools and algorithms for the construction and analysis of systems: 22nd international conference, TACAS 2016 (pp. 938\u2013941). Springer (2016)","DOI":"10.1007\/978-3-662-49674-9_65"},{"key":"1232_CR83","unstructured":"Tomassetti, F., Zaytsev, V.: Reflections on the lack of adoption of domain specific languages. In: Burgue\u00f1o, L., Kristensen, L.M. (Eds.), In: STAF Workshop proceedings (STAF) (Vol. 2707, pp. 85\u201394). CEUR-WS.org. (2020) http:\/\/ceur-ws.org\/Vol-2707\/oopslepaper5.pdf"},{"key":"1232_CR84","doi-asserted-by":"crossref","unstructured":"Usman, M., Gopinath, D., Sun, Y., Noller, Y., P\u0103s\u0103reanu, C.S.: Nnrepair: constraint-based repair of neural network classifiers. In: Silva, A., Leino, K.R.M. (Eds.), In: Computer aided verification: 33rd international conference, CAV 2021 (pp. 3\u201325). Springer (2021)","DOI":"10.1007\/978-3-030-81685-8_1"},{"key":"1232_CR85","doi-asserted-by":"crossref","unstructured":"van Dijk, T.: Oink: an implementation and evaluation of modern parity game solvers. In: Beyer, D., Huisman, M. (Eds.), In: Proceedings of the 24th international conference on tools and algorithms for the construction and analysis of systems (TACAS) (Vol. 10805, pp. 291\u2013308). Springer (2018)","DOI":"10.1007\/978-3-319-89960-2_16"},{"issue":"1","key":"1232_CR86","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1109\/MS.2019.2956701","volume":"38","author":"J Whittle","year":"2021","unstructured":"Whittle, J., Ferrario, M.A., Simm, W., Hussain, W.: A case for human values in software engineering. IEEE Softw. 38(1), 106\u2013113 (2021). https:\/\/doi.org\/10.1109\/MS.2019.2956701","journal-title":"IEEE Softw."},{"key":"1232_CR87","doi-asserted-by":"crossref","unstructured":"Wiedijk, F.: Comparing mathematical provers. In: Asperti, A. Buchberger, B., Davenport, J.H. (Eds.), In: Proceedings of the second international conference on mathematical knowledge management (MKM) (Vol. 2594, pp. 188\u2013202). Springer (2003)","DOI":"10.1007\/3-540-36469-2_15"},{"key":"1232_CR88","doi-asserted-by":"crossref","unstructured":"Wigderson, A.: Mathematics and computation: ideas revolutionizing technology and science. Princeton University Press. (2019) https:\/\/www.math.ias.edu\/avi\/book","DOI":"10.1515\/9780691192543"},{"key":"1232_CR89","doi-asserted-by":"crossref","unstructured":"Winter, S., Timperley, C.S., Hermann, B., Cito, J., Bell, J., Hilton, M., Beyer, D.: A retrospective study of one decade of artifact evaluations. In: Proceedings of the 30th ACM joint European software engineering conference and symposium on the foundations of software engineering (pp. 145\u2013156). New York, NY, USA: Association for Computing Machinery (2022)","DOI":"10.1145\/3540250.3549172"},{"key":"1232_CR90","doi-asserted-by":"crossref","unstructured":"Wolf, F.A., Arquint, L., Clochard, M., Oortwijn, W., Pereira, J.C., M\u00fcller, P.: Gobra: modular specification and verification of go programs. In: Silva, A., Leino, K.R.M. (Eds.), In: Proceedings of the 33rd international conference on computer aided verification (CAV) (Vol. 12759, pp. 367\u2013379). Springer (2021)","DOI":"10.1007\/978-3-030-81685-8_17"},{"issue":"4","key":"1232_CR91","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1592434.1592436","volume":"41","author":"J Woodcock","year":"2009","unstructured":"Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.S.: Formal methods: practice and experience. ACM Comput. Surv. 41(4), 1\u201336 (2009). https:\/\/doi.org\/10.1145\/1592434.1592436","journal-title":"ACM Comput. Surv."},{"key":"1232_CR92","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1613\/jair.2490","volume":"32","author":"L Xu","year":"2008","unstructured":"Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: Satzilla: portfolio-based algorithm selection for SAT. J. Artif. Intell. Res. 32, 565\u2013606 (2008). https:\/\/doi.org\/10.1613\/jair.2490","journal-title":"J. Artif. Intell. Res."},{"key":"1232_CR93","doi-asserted-by":"crossref","unstructured":"Zaytsev, V.: Renarrating linguistic architecture: a case study. In: Hardebolle, C., Syriani, E., Sprinkle, J., M\u00e9sz\u00e1ros, T. (Eds.), In: Post-proceedings of the sixth international workshop on multi-paradigm modeling (MPM 2012) (pp. 61\u201366). ACM Digital Library (2012)","DOI":"10.1145\/2508443.2508454"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-024-01232-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-024-01232-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-024-01232-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,6]],"date-time":"2025-09-06T02:50:39Z","timestamp":1757127039000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-024-01232-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,8]]},"references-count":93,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2025,8]]}},"alternative-id":["1232"],"URL":"https:\/\/doi.org\/10.1007\/s10270-024-01232-7","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"type":"print","value":"1619-1366"},{"type":"electronic","value":"1619-1374"}],"subject":[],"published":{"date-parts":[[2025,1,8]]},"assertion":[{"value":"6 May 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 June 2024","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 September 2024","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 January 2025","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}