{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,9]],"date-time":"2025-09-09T21:08:15Z","timestamp":1757452095723,"version":"3.40.5"},"reference-count":44,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2021,11,2]],"date-time":"2021-11-02T00:00:00Z","timestamp":1635811200000},"content-version":"unspecified","delay-in-days":1,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2021,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Assertion checking is an invaluable programmer\u2019s tool for finding many classes of errors or verifying their absence in dynamic languages such as Prolog. For Prolog programmers, this means being able to have relevant properties, such as modes, types, determinacy, nonfailure, sharing, constraints, and cost, checked and errors flagged without having to actually run the program. Such global static analysis tools are arguably most useful the earlier they are used in the software development cycle, and fast response times are essential for interactive use. Triggering a full and precise semantic analysis of a software project every time a change is made can be prohibitively expensive. This is specially the case when complex properties need to be inferred for large, realistic code bases. In our static analysis and verification framework, this challenge is addressed through a combination of modular and incremental (context- and path-sensitive) analysis that is responsive to program edits, at different levels of granularity. In this tool paper, we present how the combination of this framework within an integrated development environment (IDE) takes advantage of such incrementality to achieve a high level of reactivity when reflecting analysis and verification results back as colorings and tooltips directly on the program text \u2013 the tool\u2019s VeriFly mode. The concrete implementation that we describe is Emacs-based and reuses in part off-the-shelf \u201con-the-fly\u201d <jats:italic>syntax<\/jats:italic> checking facilities (flycheck). We believe that similar extensions are also reproducible with low effort in other mature development environments. Our initial experience with the tool shows quite promising results, with low latency times that provide early, continuous, and precise assertion checking and other semantic feedback to programmers during the development process. The tool supports Prolog natively, as well as other languages by semantic transformation into Horn clauses.<\/jats:p>","DOI":"10.1017\/s1471068421000430","type":"journal-article","created":{"date-parts":[[2021,11,2]],"date-time":"2021-11-02T09:10:41Z","timestamp":1635844241000},"page":"768-784","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":4,"title":["VeriFly: <i>On-the-fly Assertion Checking via Incrementality<\/i>"],"prefix":"10.1017","volume":"21","author":[{"given":"MIGUEL A.","family":"SANCHEZ-ORDAZ","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6098-3895","authenticated-orcid":false,"given":"ISABEL","family":"GARCIA-CONTRERAS","sequence":"additional","affiliation":[]},{"given":"VICTOR","family":"PEREZ","sequence":"additional","affiliation":[]},{"given":"JOS\u00c9 F.","family":"MORALES","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1092-2071","authenticated-orcid":false,"given":"PEDRO","family":"LOPEZ-GARCIA","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7583-323X","authenticated-orcid":false,"given":"MANUEL V.","family":"HERMENEGILDO","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2021,11,2]]},"reference":[{"key":"S1471068421000430_ref18","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000457"},{"key":"S1471068421000430_ref11","first-page":"196","article-title":"Incremental and modular context-sensitive analysis","volume":"2","author":"Garcia-Contreras","year":"2021","journal-title":"TPLP 21"},{"key":"S1471068421000430_ref8","doi-asserted-by":"crossref","unstructured":"Flanagan, C. 2006. Hybrid type checking. In 33rd ACM POPL, 245\u2013256.","DOI":"10.1145\/1111320.1111059"},{"key":"S1471068421000430_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/349214.349216"},{"key":"S1471068421000430_ref30","doi-asserted-by":"crossref","unstructured":"Perez-Carrasco, V. , Klemen, M. , Lopez-Garcia, P. , Morales, J. and Hermenegildo, M. V. 2020. Cost analysis of smart contracts via parametric resource analysis. In Static Aanalysis Simposium (SAS\u201920). LNCS, vol. 12389. Springer, 7\u201331.","DOI":"10.1007\/978-3-030-65474-0_2"},{"key":"S1471068421000430_ref12","first-page":"1409","article-title":"Decompilation of java bytecode to Prolog by partial evaluation","author":"G\u00f3mez-Zamalloa","year":"2009","journal-title":"JIST 51"},{"key":"S1471068421000430_ref28","doi-asserted-by":"crossref","unstructured":"Navas, J. , Bueno, F. and Hermenegildo, M. V. 2006. Efficient top-down set-sharing analysis using cliques. In 8th PADL. LNCS, vol. 2819. Springer, 183\u2013198.","DOI":"10.1007\/11603023_13"},{"key":"S1471068421000430_ref15","doi-asserted-by":"crossref","unstructured":"Henriksen, K. S. and Gallagher, J. P. 2006. Abstract interpretation of PIC programs through logic programming. In SCAM\u201906. IEEE Computer Society, 184\u2013196.","DOI":"10.1109\/SCAM.2006.1"},{"key":"S1471068421000430_ref17","unstructured":"Hermenegildo, M. V. , Bueno, F. , Carro, M. , Lopez-Garcia, P. , Mera, E. , Morales, J. and Puebla, G. 2011. The Ciao approach to the dynamic vs. static language dilemma. In Proc. Int\u2019l. WS on Scripts to Programs, STOP\u201911. ACM."},{"volume-title":"The Logic Programming Paradigm: A 25\u2013Year Perspective","year":"1999","author":"Hermenegildo","key":"S1471068421000430_ref19"},{"key":"S1471068421000430_ref40","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(96)00068-4"},{"key":"S1471068421000430_ref39","unstructured":"Siek, J. G. and Taha, W. 2006. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, 81\u201392."},{"key":"S1471068421000430_ref35","doi-asserted-by":"crossref","unstructured":"Puebla, G. and Hermenegildo, M. V. 1996. Optimized algorithms for the incremental analysis of logic programs. In SAS\u201996. LNCS, vol. 1145. Springer, 270\u2013284.","DOI":"10.1007\/3-540-61739-6_47"},{"key":"S1471068421000430_ref26","doi-asserted-by":"crossref","unstructured":"M\u00e9ndez-Lojo, M. , Navas, J. and Hermenegildo, M. 2007. A flexible (C)LP-based approach to the analysis of object-oriented programs. In LOPSTR. LNCS, vol. 4915. Springer-Verlag, 154\u2013168.","DOI":"10.1007\/978-3-540-78769-3_11"},{"key":"S1471068421000430_ref38","doi-asserted-by":"crossref","unstructured":"Schrijvers, T. , Santos Costa, V. , Wielemaker, J. and Demoen, B. 2008. Towards typed Prolog. In ICLP\u201908. LNCS, vol. 5366. Springer, 693\u2013697.","DOI":"10.1007\/978-3-540-89982-2_59"},{"key":"S1471068421000430_ref37","doi-asserted-by":"crossref","unstructured":"Rustan, K. , Leino, M. and W\u00fcstholz, V. 2015. Fine-grained caching of verification results. In CAV, Kroening, D. and Pasareanu, C. S. , Eds. LNCS, vol. 9206. Springer, 380\u2013397.","DOI":"10.1007\/978-3-319-21690-4_22"},{"key":"S1471068421000430_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61055-3_32"},{"volume-title":"The Goedel Programming Language","year":"1994","author":"Hill","key":"S1471068421000430_ref21"},{"key":"S1471068421000430_ref34","doi-asserted-by":"crossref","unstructured":"Puebla, G. , Bueno, F. and Hermenegildo, M. V. 2000b. Combined static and dynamic assertion-based debugging of constraint logic programs. In Proc. of LOPSTR\u201999. LNCS, vol. 1817. Springer-Verlag, 273\u2013292.","DOI":"10.1007\/10720327_16"},{"key":"S1471068421000430_ref10","doi-asserted-by":"crossref","unstructured":"Garcia-Contreras, I. , Morales, J. and Hermenegildo, M. V. 2020. Incremental analysis of logic programs with assertions and open predicates. In LOPSTR\u201919. LNCS, vol. 12042. Springer, 36\u201356.","DOI":"10.1007\/978-3-030-45260-5_3"},{"key":"S1471068421000430_ref33","doi-asserted-by":"crossref","unstructured":"Puebla, G. , Bueno, F. and Hermenegildo, M. V. 2000a. An assertion language for constraint logic programs. In Analysis and Visualization Tools for Constraint Programming. LNCS, vol. 1870. Springer-Verlag, 23\u201361.","DOI":"10.1007\/10722311_2"},{"key":"S1471068421000430_ref2","unstructured":"Bueno, F. , Carro, M. , Hermenegildo, M. V. , Lopez-Garcia, P. and (Eds.), J. M. 2021. The Ciao System. Ref. Manual (v1.20). Tech. rep. April. URL: http:\/\/ciao-lang.org."},{"key":"S1471068421000430_ref3","unstructured":"Bueno, F. , Deransart, P. , Drabent, W. , Ferrand, G. , Hermenegildo, M. V. , Maluszynski, J. and Puebla, G. 1997. On the role of semantic approximations in validation and diagnosis of constraint logic programs. In Proc. of the 3rd Int\u2019l. WS on Automated Debugging\u2013AADEBUG. U. Link\u00f6ping Press, 155\u2013170."},{"key":"S1471068421000430_ref22","doi-asserted-by":"publisher","DOI":"10.1145\/3236950.3236970"},{"key":"S1471068421000430_ref6","doi-asserted-by":"crossref","unstructured":"De Angelis, E. , Fioravanti, F. , Pettorossi, A. and Proietti, M. 2017. Semantics-based generation of verification conditions via program specialization. Science of Computer Programming 147, 78\u2013108.","DOI":"10.1016\/j.scico.2016.11.002"},{"key":"S1471068421000430_ref25","unstructured":"Marriott, K. and S\u00f8ndergaard, H. 1993. Precise and efficient groundness analysis for logic programs. Technical report 93\/7, University of Melbourne."},{"key":"S1471068421000430_ref27","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(84)90017-1"},{"key":"S1471068421000430_ref43","doi-asserted-by":"crossref","unstructured":"Tschannen, J. , Furia, C. A. , Nordio, M. and Meyer, B. 2011. Usable verification of object-oriented programs by combining static and dynamic techniques. In SEFM. LNCS, vol. 7041. Springer, 382\u2013398.","DOI":"10.1007\/978-3-642-24690-6_26"},{"key":"S1471068421000430_ref16","doi-asserted-by":"crossref","unstructured":"Hermenegildo, M. , Puebla, G. , Bueno, F. and Garcia, P. L. 2005. Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor). Science of Computer Programming 58, 1\u20132, 115\u2013140.","DOI":"10.1016\/j.scico.2005.02.006"},{"key":"S1471068421000430_ref44","doi-asserted-by":"crossref","unstructured":"Wingen, I. and K\u00f6rner, P. 2020. Effectiveness of annotation-based static type inference. In WS on Functional and Constraint Logic Programming. LNCS, vol. 12560. Springer, 74\u201393.","DOI":"10.1007\/978-3-030-75333-7_5"},{"key":"S1471068421000430_ref14","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A. , Kahsai, T. , Komuravelli, A. and Navas, J. A. 2015. The SeaHorn verification framework. In CAV, 343\u2013361.","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"S1471068421000430_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_46"},{"volume-title":"Types in Logic Programming","year":"1992","author":"Pfenning","key":"S1471068421000430_ref31"},{"key":"S1471068421000430_ref5","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068421000211"},{"key":"S1471068421000430_ref41","doi-asserted-by":"crossref","unstructured":"Stulova, N. , Morales, J. F. and Hermenegildo, M. V. 2018a. Exploiting term hiding to reduce run-time checking overhead. In Int\u2019l. Symp. on Practical Aspects of Declarative Languages (PADL). LNCS, vol. 10702. Springer-Verlag, 99\u2013115.","DOI":"10.1007\/978-3-319-73305-0_7"},{"key":"S1471068421000430_ref36","doi-asserted-by":"crossref","unstructured":"Rastogi, A. , Swamy, N. , Fournet, C. , Bierman, G. and Vekris, P. 2015. Safe & efficient gradual typing for TypeScript. In 42nd POPL. ACM, 167\u2013180.","DOI":"10.1145\/2676726.2676971"},{"key":"S1471068421000430_ref4","doi-asserted-by":"crossref","unstructured":"Cousot, P. and Cousot, R. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In ACM Symposium on Principles of Programming Languages (POPL\u201977). ACM Press, 238\u2013252.","DOI":"10.1145\/512950.512973"},{"key":"S1471068421000430_ref24","doi-asserted-by":"crossref","unstructured":"Lopez-Garcia, P. , Darmawan, L. , Klemen, M. , Liqat, U. , Bueno, F. and Hermenegildo, M. V. 2018. Interval-based resource usage verification by translation into Horn clauses and an application to energy consumption. TPLP 18, 2, 167\u2013223.","DOI":"10.1017\/S1471068418000042"},{"key":"S1471068421000430_ref23","unstructured":"Lakshman, T. and Reddy, U. 1991. Typed Prolog: a semantic reconstruction of the Mycroft-O\u2019Keefe type system. In International Logic Programming Symposium. MIT Press."},{"key":"S1471068421000430_ref32","doi-asserted-by":"crossref","unstructured":"Pietrzak, P. , Correas, J. , Puebla, G. and Hermenegildo, M. V. 2006. Context-sensitive multivariant assertion checking in modular programs. In LPAR\u201906. LNCS, vol. 4246. Springer-Verlag, 392\u2013406.","DOI":"10.1007\/11916277_27"},{"key":"S1471068421000430_ref29","doi-asserted-by":"crossref","unstructured":"Peralta, J. , Gallagher, J. and Sa\u011flam, H. 1998. Analysis of imperative programs through analysis of constraint logic programs. In Static Analysis. 5th International Symposium, SAS\u201998, Pisa, G. Levi, Ed. LNCS, vol. 1503, 246\u2013261.","DOI":"10.1007\/3-540-49727-7_15"},{"key":"S1471068421000430_ref42","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.12.006"},{"key":"S1471068421000430_ref7","unstructured":"Dumortier, V. , Janssens, G. , Simoens, W. and Garc\u00eda de la Banda, M. 1993. Combining a definiteness and a freeness abstraction for CLP languages. In Workshop on LP Synthesis and Transformation."},{"key":"S1471068421000430_ref9","doi-asserted-by":"crossref","unstructured":"Gallagher, J. , Hermenegildo, M. V. , Kafle, B. , Klemen, M. , Lopez-Garcia, P. and Morales, J. 2020. From big-step to small-step semantics and back with interpreter specialization. In VPT 2020. EPTCS. Open Publishing Association, 50\u201365.","DOI":"10.4204\/EPTCS.320.4"}],"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\/S1471068421000430","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T10:17:27Z","timestamp":1641464247000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068421000430\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11]]},"references-count":44,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2021,11]]}},"alternative-id":["S1471068421000430"],"URL":"https:\/\/doi.org\/10.1017\/s1471068421000430","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"type":"print","value":"1471-0684"},{"type":"electronic","value":"1475-3081"}],"subject":[],"published":{"date-parts":[[2021,11]]},"assertion":[{"value":"\u00a9 The Author(s), 2021. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}