{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,17]],"date-time":"2026-06-17T13:54:01Z","timestamp":1781704441554,"version":"3.54.5"},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T00:00:00Z","timestamp":1773619200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T00:00:00Z","timestamp":1773619200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100007241","name":"Universit\u00e9 Paris-Saclay","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100007241","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2026,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    This paper proposes a semantic static analysis for inferring nullable or non-null pointer annotations in low level programs. The analysis is formulated on a minimalistic imperative language and it is expressed as a least fixpoint computation over pointer annotations calling a sound type-checking algorithm. Therefore, this analysis may be used for more general annotations than pointer nullability. We prove two main properties for this approach: (1) when using a sound and precise type-checker (i.e., without false alarms), it will find an annotation that guarantees the absence of run-time errors due to pointer deference, if such an annotation exists, (2) when the type-checker is only sound, the errors singled out by the analysis are real errors. We report on the implementation of this method in\n                    <jats:sc>Codex<\/jats:sc>\n                    , a static analyzer for C and binary code.\n                    <jats:sc>Codex<\/jats:sc>\n                    already provides an abstract interpretation based type-checker for a rich dependent type systems. The evaluation of our implementation on a benchmark of challenging programs shows that the inference is better than manual annotations obtained by code inspection.\n                  <\/jats:p>","DOI":"10.1007\/s10009-026-00846-0","type":"journal-article","created":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T17:15:04Z","timestamp":1773681304000},"page":"303-316","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Inferring contracts by abstract interpretation with application to pointer nullness analysis"],"prefix":"10.1007","volume":"28","author":[{"given":"Paul","family":"Robert","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthieu","family":"Lemerre","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mihaela","family":"Sighireanu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,3,16]]},"reference":[{"key":"846_CR1","series-title":"Lecture Notes in Computer Science","isbn-type":"print","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-642-35182-2_13","volume-title":"Programming Languages and Systems - 10th Asian Symposium, APLAS 2012, Kyoto, Japan, December 11-13, 2012, Proceedings","author":"M. Bouaziz","year":"2012","unstructured":"Bouaziz, M., Logozzo, F., F\u00e4hndrich, M.: Inference of necessary field conditions with abstract interpretation. In: Jhala, R., Igarashi, A. (eds.) Programming Languages and Systems - 10th Asian Symposium, APLAS 2012, Kyoto, Japan, December 11-13, 2012, Proceedings. Lecture Notes in Computer Science, vol.\u00a07705, pp.\u00a0173\u2013189. Springer, Berlin (2012). ISBN 978-3-642-35181-5, 978-3-642-35182-2. https:\/\/doi.org\/10.1007\/978-3-642-35182-2_13","ISBN":"https:\/\/id.crossref.org\/isbn\/9783642351815"},{"key":"846_CR2","unstructured":"CODEX: (2025). https:\/\/codex.top"},{"issue":"8","key":"846_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/872734.806926","volume":"12","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Automatic synthesis of optimal invariant assertions: mathematical foundations. ACM SIGPLAN Not. 12(8), 1\u201312 (1977)","journal-title":"ACM SIGPLAN Not."},{"key":"846_CR4","unstructured":"Dunkels, A.: Contiki-os (2023). https:\/\/github.com\/contiki-ng\/contiki-ng\/blob\/master\/os\/lib\/list.c"},{"key":"846_CR5","series-title":"LIPIcs","doi-asserted-by":"publisher","first-page":"3:1","DOI":"10.4230\/LIPICS.ECOOP.2021.3","volume-title":"35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11-17, 2021, Aarhus, Denmark, Virtual Conference","author":"S. Estep","year":"2021","unstructured":"Estep, S., Wise, J., Aldrich, J., Tanter, \u00c9., Bader, J., Sunshine, J.: Gradual program analysis for null pointers. In: M\u00f8ller, A., Sridharan, M. (eds.) 35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11-17, 2021, Aarhus, Denmark, Virtual Conference. LIPIcs, vol.\u00a0194, pp.\u00a03:1\u20133:25. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2021.3"},{"key":"846_CR6","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1145\/949305.949332","volume-title":"Proceedings of the 18th Annual ACM SIGPLAN Conference on Object-Oriented Programing, Systems, Languages, and Applications, OOPSLA \u201903","author":"M. F\u00e4hndrich","year":"2003","unstructured":"F\u00e4hndrich, M., Leino, K.R.M.: Declaring and checking non-null types in an object-oriented language. In: Proceedings of the 18th Annual ACM SIGPLAN Conference on Object-Oriented Programing, Systems, Languages, and Applications, OOPSLA \u201903, pp.\u00a0302\u2013312. Association for Computing Machinery, New York (2003). ISBN 1581137125. https:\/\/doi.org\/10.1145\/949305.949332"},{"key":"846_CR7","volume-title":"InfoQ Conference","author":"T. Hoare","year":"2009","unstructured":"Hoare, T.: Null references: the billion dollar mistake. In: InfoQ Conference (2009)"},{"key":"846_CR8","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-540-68863-1_9","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"L. Hubert","year":"2008","unstructured":"Hubert, L., Jensen, T., Pichardie, D.: Semantic foundations and inference of non-null annotations. In: Barthe, G., De Boer, F.S. (eds.) Formal Methods for Open Object-Based Distributed Systems, vol.\u00a05051, pp.\u00a0132\u2013149. Springer, Berlin (2008). https:\/\/doi.org\/10.1007\/978-3-540-68863-1_9. ISBN 978-3-540-68862-4, 978-3-540-68863-1. http:\/\/link.springer.com\/10.1007\/978-3-540-68863-1_9"},{"key":"846_CR9","isbn-type":"print","doi-asserted-by":"publisher","first-page":"1395","DOI":"10.1145\/3611643.3616326","volume-title":"Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","author":"N. Karimipour","year":"2023","unstructured":"Karimipour, N., Pham, J., Clapp, L., Sridharan, M.: Practical inference of nullability types. In: Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp.\u00a01395\u20131406. ACM, New York (2023). ISBN 979-8-4007-0327-0. https:\/\/doi.org\/10.1145\/3611643.3616326. https:\/\/dl.acm.org\/doi\/10.1145\/3611643.3616326","ISBN":"https:\/\/id.crossref.org\/isbn\/9798400703270"},{"key":"846_CR10","isbn-type":"print","doi-asserted-by":"publisher","first-page":"1542","DOI":"10.1109\/ASE56229.2023.00186","volume-title":"2023 38th IEEE\/ACM International Conference on Automated Software Engineering","author":"M. Kellogg","year":"2023","unstructured":"Kellogg, M., Daskiewicz, D., Duc Nguyen, L.N., Ahmed, M., Ernst, M.D.: Pluggable type inference for free. In: 2023 38th IEEE\/ACM International Conference on Automated Software Engineering, ASE, Luxembourg, Luxembourg, Sept. 2023, pp.\u00a01542\u20131554. IEEE (2023). ISBN 979-8-3503-2996-4. https:\/\/doi.org\/10.1109\/ASE56229.2023.00186","ISBN":"https:\/\/id.crossref.org\/isbn\/9798350329964"},{"key":"846_CR11","doi-asserted-by":"publisher","unstructured":"Machiry, A., Kastner, J.H., McCutchen, M., Eline, A., Headley, K., Hicks, M.: C to checked C by 3c (with appendices) (2022). CoRR arXiv:2203.13445. https:\/\/doi.org\/10.48550\/arXiv.2203.13445","DOI":"10.48550\/arXiv.2203.13445"},{"issue":"10","key":"846_CR12","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B. Meyer","year":"1992","unstructured":"Meyer, B.: Applying \u201cdesign by contract\u201d. Computer 25(10), 40\u201351 (1992). https:\/\/doi.org\/10.1109\/2.161279","journal-title":"Computer"},{"key":"846_CR13","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/1390630.1390656","volume-title":"Proceedings of the ACM\/SIGSOFT International Symposium on Software Testing and Analysis","author":"M.M. Papi","year":"2008","unstructured":"Papi, M.M., Ali, M., Correa, T.L.\u00a0Jr., Perkins, J.H., Ernst, M.D.: Practical pluggable types for Java. In: Ryder, B.G., Zeller, A. (eds.) Proceedings of the ACM\/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2008, Seattle, WA, USA, July 20-24, 2008, pp.\u00a0201\u2013212. ACM (2008). https:\/\/doi.org\/10.1145\/1390630.1390656"},{"key":"846_CR14","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1145\/1706299.1706316","volume-title":"POPL","author":"P.M. Rondon","year":"2010","unstructured":"Rondon, P.M., Kawaguchi, M., Jhala, R.: Low-level liquid types. In: POPL, pp.\u00a0131\u2013144. ACM, New York (2010). https:\/\/doi.org\/10.1145\/1706299.1706316"},{"issue":"OOPSLA2","key":"846_CR15","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/3689712","volume":"8","author":"J. Simonnet","year":"2024","unstructured":"Simonnet, J., Lemerre, M., Sighireanu, M.: A dependent nominal physical type system for static analysis of memory in low level code. Proc. ACM Program. Lang. 8(OOPSLA2), 30\u201359 (2024). https:\/\/doi.org\/10.1145\/3689712","journal-title":"Proc. ACM Program. Lang."},{"key":"846_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-031-74776-2_17","volume-title":"Static Analysis - 31st International Symposium, SAS 2024, Pasadena, CA, USA, October 20-22, 2024, Proceedings","author":"I. Smith","year":"2024","unstructured":"Smith, I.: Binsub: the simple essence of polymorphic type inference for machine code. In: Giacobazzi, R., Gorla, A. (eds.) Static Analysis - 31st International Symposium, SAS 2024, Pasadena, CA, USA, October 20-22, 2024, Proceedings. Lecture Notes in Computer Science, vol.\u00a014995, pp.\u00a0425\u2013450. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-74776-2_17"},{"issue":"2","key":"846_CR17","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10270-009-0132-5","volume":"10","author":"F. Spoto","year":"2011","unstructured":"Spoto, F.: Precise null-pointer analysis. Softw. Syst. Model. 10(2), 219\u2013252 (2011)","journal-title":"Softw. Syst. Model."},{"key":"846_CR18","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1145\/292540.292560","volume-title":"Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"H. Xi","year":"1999","unstructured":"Xi, H., Pfenning, F.: Dependent types in practical programming. In: Appel, A.W., Aiken, A. (eds.) Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201999, San Antonio, TX, USA, January 20-22, 1999, pp.\u00a0214\u2013227. ACM (1999). https:\/\/doi.org\/10.1145\/292540.292560"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-026-00846-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-026-00846-0","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-026-00846-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,17]],"date-time":"2026-06-17T13:05:45Z","timestamp":1781701545000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-026-00846-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,16]]},"references-count":18,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2026,6]]}},"alternative-id":["846"],"URL":"https:\/\/doi.org\/10.1007\/s10009-026-00846-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,3,16]]},"assertion":[{"value":"20 February 2026","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 March 2026","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}