{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:03:35Z","timestamp":1776305015593,"version":"3.50.1"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031713781","type":"print"},{"value":"9783031713798","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:00:00Z","timestamp":1725494400000},"content-version":"vor","delay-in-days":248,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Nowadays, ready-to-use libraries and code generation are often used to streamline and speed up the software development process. The resulting programs are thus a collection of different modules that cooperate: proving their safety and reliability is increasingly complex, requiring sound formal techniques, such as static program analysis. However, while teaching static analysis to master\u2019s or PhD students, the predominant focus on theoretical concepts often leaves limited space for students to engage with the practical aspects of implementing static analyses and is limited to developing elementary ones. In this paper, we show how the infrastructure offered by LiSA can be exploited to learn how to implement advanced static analyses, such as string and relational numerical analyses, just focusing on their distinctive aspects. This would help to narrow the gap between theoretical and practical contents in static analysis courses, bringing the learning experience beyond the rudimentary implementation of static analyses to more sophisticated applications.<\/jats:p>","DOI":"10.1007\/978-3-031-71379-8_3","type":"book-chapter","created":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T14:02:25Z","timestamp":1725458545000},"page":"43-57","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Teaching Through Practice: Advanced Static Analysis with\u00a0LiSA"],"prefix":"10.1007","author":[{"given":"Luca","family":"Negrini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vincenzo","family":"Arceri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Olivieri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Agostino","family":"Cortesi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pietro","family":"Ferrara","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,9,5]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","unstructured":"Allen, F.E.: Control Flow Analysis. In: Proceedings of a Symposium on Compiler Optimization, p. 1\u201319. Association for Computing Machinery, New York, NY, USA (1970). https:\/\/doi.org\/10.1145\/800028.808479","DOI":"10.1145\/800028.808479"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-030-94583-1_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"V Arceri","year":"2022","unstructured":"Arceri, V., Olliaro, M., Cortesi, A., Ferrara, P.: Relational string abstract domains. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 20\u201342. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_2"},{"key":"3_CR3","doi-asserted-by":"publisher","unstructured":"Becchi, A., Zaffanella, E.: PPlite: zero-overhead encoding of NNC polyhedra. Inf. Comput. 275, 104620 (2020). https:\/\/doi.org\/10.1016\/J.IC.2020.104620","DOI":"10.1016\/J.IC.2020.104620"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44898-5_1","volume-title":"Static Analysis","author":"AS Christensen","year":"2003","unstructured":"Christensen, A.S., M\u00f8ller, A., Schwartzbach, M.I.: Precise analysis of string expressions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 1\u201318. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-44898-5_1"},{"key":"3_CR5","doi-asserted-by":"publisher","unstructured":"Costantini, G., Ferrara, P., Cortesi, A.: A suite of abstract domains for static analysis of string values. Softw. Pract. Exp. 45(2), 245\u2013287 (2015). https:\/\/doi.org\/10.1002\/SPE.2218","DOI":"10.1002\/SPE.2218"},{"key":"3_CR6","unstructured":"Cousot, P.: Principles of Abstract Interpretation. MIT Press (2021)"},{"key":"3_CR7","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pp. 238\u2013252. ACM (1977). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"3_CR8","doi-asserted-by":"publisher","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Aho, A.V., Zilles, S.N., Szymanski, T.G. (eds.) Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, USA, January 1978, pp. 84\u201396. ACM Press (1978). https:\/\/doi.org\/10.1145\/512760.512770","DOI":"10.1145\/512760.512770"},{"key":"3_CR9","doi-asserted-by":"publisher","unstructured":"Cowan, C., Wagle, F., Pu, C., Beattie, S., Walpole, J.: Buffer overflows: attacks and defenses for the vulnerability of the decade. In: Proceedings DARPA Information Survivability Conference and Exposition. DISCEX\u201900, vol.\u00a02, vol. 2, pp. 119\u2013129 (2000). https:\/\/doi.org\/10.1109\/DISCEX.2000.821514","DOI":"10.1109\/DISCEX.2000.821514"},{"key":"3_CR10","doi-asserted-by":"publisher","unstructured":"Ferrara, P., Negrini, L., Arceri, V., Cortesi, A.: Static analysis for dummies: experiencing lisa. In: Do, L.N.Q., Urban, C. (eds.) SOAP@PLDI 2021: Proceedings of the 10th ACM SIGPLAN International Workshop on the State of the Art in Program Analysis, Virtual Event, Canada, 22 June, 2021, pp.\u00a01\u20136. ACM (2021). https:\/\/doi.org\/10.1145\/3460946.3464316","DOI":"10.1145\/3460946.3464316"},{"issue":"07","key":"3_CR11","doi-asserted-by":"publisher","first-page":"973","DOI":"10.1142\/S0218194021500303","volume":"31","author":"P Ferrara","year":"2021","unstructured":"Ferrara, P., Olivieri, L., Spoto, F.: Static privacy analysis by flow reconstruction of tainted data. Int. J. Softw. Eng. Know. Eng. 31(07), 973\u20131016 (2021). https:\/\/doi.org\/10.1142\/S0218194021500303","journal-title":"Int. J. Softw. Eng. Know. Eng."},{"key":"3_CR12","doi-asserted-by":"publisher","unstructured":"Logozzo, F., F\u00e4hndrich, M.: Pentagons: a weakly relational abstract domain for the efficient validation of array accesses. Sci. Comput. Program. 75(9), 796\u2013807 (2010). https:\/\/doi.org\/10.1016\/J.SCICO.2009.04.004","DOI":"10.1016\/J.SCICO.2009.04.004"},{"key":"3_CR13","doi-asserted-by":"publisher","unstructured":"Min\u00e9, A.: The octagon abstract domain. High. Order Symb. Comput. 19(1), 31\u2013100 (2006). https:\/\/doi.org\/10.1007\/S10990-006-8609-1","DOI":"10.1007\/S10990-006-8609-1"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-030-67067-2_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L Negrini","year":"2021","unstructured":"Negrini, L., Arceri, V., Ferrara, P., Cortesi, A.: Twinning automata and regular expressions for string static analysis. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) VMCAI 2021. LNCS, vol. 12597, pp. 267\u2013290. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-67067-2_13"},{"key":"3_CR15","doi-asserted-by":"publisher","unstructured":"Negrini, L., Ferrara, P., Arceri, V., Cortesi, A.: LiSA: a Generic Framework for Multilanguage Static Analysis. In: Arceri, V., Cortesi, A., Ferrara, P., Olliaro, M. (eds.) Challenges of Software Verification. Intelligent Systems Reference Library, vol. 238, pp. 19\u201342 Springer, Singapore (2023). https:\/\/doi.org\/10.1007\/978-981-19-9601-6_2","DOI":"10.1007\/978-981-19-9601-6_2"},{"key":"3_CR16","doi-asserted-by":"publisher","unstructured":"Negrini, L., Shabadi, G., Urban, C.: Static analysis of data transformations in Jupyter notebooks. In: Ferrara, P., Hadarean, L. (eds.) Proceedings of the 12th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, SOAP 2023, Orlando, FL, USA, 17 June 2023, pp. 8\u201313. ACM (2023). https:\/\/doi.org\/10.1145\/3589250.3596145","DOI":"10.1145\/3589250.3596145"},{"key":"3_CR17","doi-asserted-by":"publisher","unstructured":"Olivieri, L., Jensen, T.P., Negrini, L., Spoto, F.: MichelsonLiSA: a static analyzer for Tezos. In: IEEE International Conference on Pervasive Computing and Communications Workshops and other Affiliated Events, PerCom Workshops 2023, Atlanta, GA, USA, 13-17 March 2023, pp. 80\u201385. IEEE (2023). https:\/\/doi.org\/10.1109\/PERCOMWORKSHOPS56833.2023.10150247","DOI":"10.1109\/PERCOMWORKSHOPS56833.2023.10150247"},{"key":"3_CR18","doi-asserted-by":"publisher","unstructured":"Olivieri, L., et al.: Information flow analysis for detecting non-determinism in blockchain. In: Ali, K., Salvaneschi, G. (eds.) 37th European Conference on Object-Oriented Programming, ECOOP 2023, 17-21 July 2023, Seattle, Washington, United States. LIPIcs, vol.\u00a0263, pp. 23:1\u201323:25. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2023.23","DOI":"10.4230\/LIPICS.ECOOP.2023.23"},{"issue":"1","key":"3_CR19","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A Sabelfeld","year":"2006","unstructured":"Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. A. Commun. 21(1), 5\u201319 (2006)","journal-title":"IEEE J. Sel. A. Commun."},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Schwarz, M., Seidl, H.: Octagons revisited - elegant proofs and simplified algorithms. In: Hermenegildo, M.V., Morales, J.F. (eds.) Static Analysis - 30th International Symposium, SAS 2023, Cascais, Portugal, October 22-24, 2023, Proceedings. Lecture Notes in Computer Science, vol. 14284, pp. 485\u2013507. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-44245-2_21","DOI":"10.1007\/978-3-031-44245-2_21"},{"key":"3_CR21","doi-asserted-by":"publisher","unstructured":"Spoto, F., et al.: Static identification of injection attacks in Java. ACM Trans. Program. Lang. Syst. 41(3) (2019). https:\/\/doi.org\/10.1145\/3332371","DOI":"10.1145\/3332371"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-642-39274-0_3","volume-title":"Implementation and Application of Automata","author":"M Veanes","year":"2013","unstructured":"Veanes, M.: Applications of symbolic finite automata. In: Konstantinidis, S. (ed.) CIAA 2013. LNCS, vol. 7982, pp. 16\u201323. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39274-0_3"}],"container-title":["Lecture Notes in Computer Science","Formal Methods Teaching"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71379-8_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T14:03:15Z","timestamp":1725458595000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71379-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031713781","9783031713798"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71379-8_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"5 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FMTea","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Formal Methods Teaching Workshop","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tfm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/?page_id=423","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}