{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T05:30:33Z","timestamp":1737005433519,"version":"3.33.0"},"reference-count":60,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2024,10,31]],"date-time":"2024-10-31T00:00:00Z","timestamp":1730332800000},"content-version":"unspecified","delay-in-days":60,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2024,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This technical note shows how we have combined prescriptive type checking and constraint solving to increase automation during software verification. We do so by defining a type system and implementing a typechecker for <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S1471068424000206_inline1.png\"\/><jats:tex-math>\n$\\{log\\}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> (read \u2018setlog\u2019), a Constraint Logic Programming language and satisfiability solver based on set theory. The constraint solver is proved to be safe w.r.t. the type system. Two industrial-strength case studies are presented where this combination is used with very good results.<\/jats:p>","DOI":"10.1017\/s1471068424000206","type":"journal-article","created":{"date-parts":[[2024,10,31]],"date-time":"2024-10-31T11:19:10Z","timestamp":1730373550000},"page":"1011-1030","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["Combining Type Checking and Set Constraint Solving to Improve Automated Software Verification"],"prefix":"10.1017","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9163-2609","authenticated-orcid":false,"given":"MAXIMILIANO","family":"CRISTI\u00c1","sequence":"first","affiliation":[]},{"given":"GIANFRANCO","family":"ROSSI","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2024,10,31]]},"reference":[{"key":"S1471068424000206_ref51","doi-asserted-by":"crossref","unstructured":"Pietrzak, P. , Correas, J. , Puebla, G. and Hermenegildo, M. V. 2008. A practical type analysis for verification of modular prolog programs. Gl\u00fcck, R. and de Moor, O , Eds. In Proceedings of the 2008 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation, PEPM. 2008, January 7-8, 2008, San Francisco, California, USA, 61\u201370.","DOI":"10.1145\/1328408.1328418"},{"volume-title":"Types in logic programming","year":"1992","author":"Pfenning","key":"S1471068424000206_ref1"},{"key":"S1471068424000206_ref11","unstructured":"Bruynooghe, M. and Janssens, G. 1988. An instance of abstract interpretation integrating type and mode inferencing. Kowalski, R. A. and Bowen, K. A , Eds. In Logic Programming, Proceedings of the Fifth International Conference and Symposium, MIT Press, Seattle, Washington, USA, 669\u2013683."},{"key":"S1471068424000206_ref40","doi-asserted-by":"publisher","DOI":"10.1145\/319301.319317"},{"key":"S1471068424000206_ref43","doi-asserted-by":"publisher","DOI":"10.19153\/cleiej.21.2.3"},{"key":"S1471068424000206_ref28","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068406002730"},{"key":"S1471068424000206_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/365151.365169"},{"key":"S1471068424000206_ref58","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"S1471068424000206_ref25","first-page":"157","volume-title":"Types in Logic Programming","author":"Dart","year":"1992"},{"key":"S1471068424000206_ref60","unstructured":"Zobel, J. 1987. Derivation of polymorphic types for PROLOG programs. Lassez, J. , Eds. In Logic Programming, Proceedings of the Fourth International Conference, May 25-29, 1987, MIT Press, Melbourne, Victoria, Australia, 2, 817\u2013838."},{"key":"S1471068424000206_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-023-09666-2"},{"key":"S1471068424000206_ref33","first-page":"123","volume-title":"Programming Logics - Essays in Memory of Harald Ganzinger","volume":"7797","author":"Hanus","year":"2013"},{"key":"S1471068424000206_ref39","unstructured":"Lakshman, T. L. and Reddy, U. S. 1991. Typed Prolog: A semantic reconstruction of the Mycroft-O\u2019Keefe type system. Saraswat, V. A. and Ueda, K. , Eds. In Logic Programming, Proceedings of the 1991 International Symposium, Oct. 28 - Nov. 1, 1991, MIT Press, San Diego, California, USA, 202\u2013217."},{"key":"S1471068424000206_ref44","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0391-0"},{"key":"S1471068424000206_ref52","unstructured":"Rossi, G. (2008). {log}. Available at http:\/\/www.clpset.unipr.it\/setlog.Home.html. Last access 2022."},{"key":"S1471068424000206_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"S1471068424000206_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-021-09602-2"},{"key":"S1471068424000206_ref37","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.02.006"},{"key":"S1471068424000206_ref21","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068421000521"},{"key":"S1471068424000206_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-021-09589-w"},{"key":"S1471068424000206_ref36","first-page":"141","volume-title":"Types in Logic Programming","author":"Heintze","year":"1992"},{"key":"S1471068424000206_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02149-8_20"},{"key":"S1471068424000206_ref15","unstructured":"Cristi\u00e1, M. and Rossi, G. 2019. Rewrite rule s for a solver for sets, binary relations and partial functions. Tech. rep. Available at: https:\/\/www.clpset.unipr.it\/SETLOG\/calculus.pdf. [Accessed on August, 20, 2023]."},{"volume-title":"The Z Notation: A Reference Manual","year":"1992","author":"Spivey","key":"S1471068424000206_ref55"},{"key":"S1471068424000206_ref7","doi-asserted-by":"crossref","unstructured":"Betarte, G. , Campo, J. D. , Luna, C. D. and Romano, A. 2015. Verifying android\u2019s permission model. Leucker, M. , Rueda, C. and Valencia, F. D , Eds. Lecture Notes in Computer Science. In Theoretical Aspects of Computing - ICTAC 2015 - 12th International Colloquium, Proceedings, October 29-31, 2015, 9399, Springer, Cali, Colombia, 485\u2013504.","DOI":"10.1007\/978-3-319-25150-9_28"},{"key":"S1471068424000206_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09520-4"},{"key":"S1471068424000206_ref4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881"},{"key":"S1471068424000206_ref32","unstructured":"Gallagher, J. P. and de Waal, D. A. 1994. Fast and precise regular approximations of logic programs. Hentenryck, P. V. , Eds. In Logic Programming, Proceedings of the Eleventh International Conference on Logic Programming, June 13-18, 1994, MIT Press, Santa Marherita Ligure, Italy, 599\u2013613."},{"key":"S1471068424000206_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75560-9_13"},{"key":"S1471068424000206_ref22","first-page":"56","volume-title":"From Computational Logic to Computational Biology - Essays Dedicated to Alfredo Ferro to Celebrate His Scientific Career","volume":"14070","author":"Cristi\u00e1","year":"2024"},{"key":"S1471068424000206_ref49","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(84)90017-1"},{"key":"S1471068424000206_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0145-y"},{"key":"S1471068424000206_ref12","unstructured":"Cirstea, H. , Coquery, E. , Drabent, W. , Fages, F. , Kirchner, C. , Maluszynski, J. and Wack, B. 2004. Types for web rule languages: a preliminary study. Contract A04-R-560, Inria. Rapport de contrat. https:\/\/hal.inria.fr\/inria-00099859\/file\/A04-R-560.pdf"},{"key":"S1471068424000206_ref24","first-page":"229","volume-title":"{log} as a test case generator for the test template framework","volume":"8137","author":"Cristi\u00e1","year":"2013"},{"key":"S1471068424000206_ref45","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07512-9_6"},{"key":"S1471068424000206_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09577-6"},{"key":"S1471068424000206_ref26","unstructured":"De Luca, G. and Luna, C. 2020. Towards a certified reference monitor of the android 10 permission system. de\u2019Liguoro, U. , Berardi, S. and Altenkirch, T. , Eds. In 26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy, LIPIcs, 188, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 3:1-3:18."},{"key":"S1471068424000206_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/3625230"},{"volume-title":"The G\u00f6del Programming Language","year":"1994","author":"Hill","key":"S1471068424000206_ref38"},{"key":"S1471068424000206_ref31","doi-asserted-by":"crossref","unstructured":"Fr\u00fchwirth, T. W. , Shapiro, E. , Vardi, M. Y. and Yardeni, E. 1991. Logic programs as types for logic programs. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS \u201991), July 15-18, 1991, IEEE Computer Society, Amsterdam, The Netherlands, 300\u2013309.","DOI":"10.1109\/LICS.1991.151654"},{"key":"S1471068424000206_ref48","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"S1471068424000206_ref34","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781316576892"},{"key":"S1471068424000206_ref47","first-page":"238","volume-title":"Discharging proof obligations from atelier B using multiple automated provers","volume":"7316","author":"Mentr\u00e9","year":"2012"},{"key":"S1471068424000206_ref5","doi-asserted-by":"crossref","unstructured":"Barbosa, J. , Florido, M. and Costa, V. S. 2021. Data type inference for logic programming. Angelis, E. D. and Vanhoof, W , Eds. Lecture Notes in Computer Science, In Logic-Based Program Synthesis and Transformation - 31st International Symposium, LOPSTR. 2021, Proceedings, September 7-8, 2021, Tallinn, Estonia, Springer, 13290, 16\u201337.","DOI":"10.1007\/978-3-030-98869-2_2"},{"key":"S1471068424000206_ref46","article-title":"Intuitionistic type theory","volume":"1","author":"Martin-L\u00f6f","year":"1984","journal-title":"Studies in Proof Theory"},{"key":"S1471068424000206_ref57","unstructured":"Vaucheret, C. and Bueno, F. 2002. More precise yet efficient type inference for logic programs. Tessier, A. , Eds. In Proceedings of the 12th International Workshop on Logic Programming Environments, WLPE 2002, July 31, 2002, Copenhagen, Denmark, 63\u201376."},{"key":"S1471068424000206_ref8","doi-asserted-by":"publisher","DOI":"10.7561\/SACS.2016.1.27"},{"key":"S1471068424000206_ref59","first-page":"63","volume-title":"Types in Logic Programming","author":"Yardeni","year":"1992"},{"key":"S1471068424000206_ref20","unstructured":"Cristi\u00e1, M. and Rossi, G. 2022. Combining type checking and set constraint solving to improve automated software verification. CoRR abs\/2205.01713v2. Extended version \u2013 arXiv: 2205.01713v2. https:\/\/arxiv.org\/pdf\/2205.0.1713v2."},{"key":"S1471068424000206_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07512-9_1"},{"volume-title":"Types and Programming Languages","year":"2002","author":"Pierce","key":"S1471068424000206_ref50"},{"key":"S1471068424000206_ref41","doi-asserted-by":"crossref","unstructured":"Leuschel, M. 2020. Prolog for verification, analysis and transformation tools. Fribourg, L. and Heizmann, M. , Eds. In Proceedings 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis, VPT\/HCVS@ETAPS. 2020, 25-26th April 2020, EPTCS, Dublin, Ireland, 320, 80\u201394.","DOI":"10.4204\/EPTCS.320.0"},{"key":"S1471068424000206_ref53","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89982-2_59"},{"key":"S1471068424000206_ref30","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068401001120"},{"key":"S1471068424000206_ref35","doi-asserted-by":"crossref","unstructured":"Heintze, N. and Jaffar, J. 1990. A finite presentation theorem for approximating logic programs. Allen, F. E. , Ed. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, January 1990, San Francisco, California, USA, ACM Press, 197\u2013209.","DOI":"10.1145\/96709.96729"},{"key":"S1471068424000206_ref54","doi-asserted-by":"crossref","unstructured":"Somogyi, Z. , Henderson, F. and Conway, T. C. 1996. The execution algorithm of mercury, an efficient purely declarative logic programming language, 29:1\u20133,17-64.","DOI":"10.1016\/S0743-1066(96)00068-4"},{"key":"S1471068424000206_ref42","first-page":"855","volume-title":"ProB: a model checker for B","volume":"2805","author":"Leuschel","year":"2003"},{"key":"S1471068424000206_ref56","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0032738"},{"key":"S1471068424000206_ref6","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139032636"},{"key":"S1471068424000206_ref29","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068402001473"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068424000206","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,15]],"date-time":"2025-01-15T13:50:22Z","timestamp":1736949022000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068424000206\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9]]},"references-count":60,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2024,9]]}},"alternative-id":["S1471068424000206"],"URL":"https:\/\/doi.org\/10.1017\/s1471068424000206","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"type":"print","value":"1471-0684"},{"type":"electronic","value":"1475-3081"}],"subject":[],"published":{"date-parts":[[2024,9]]},"assertion":[{"value":"\u00a9 The Author(s), 2024. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}