Programming Languages and Compilers

2024

• R. Giacobazzi, I. Mastroeni, and E. Perantoni. Adversities in Abstract Interpretation - Accommodating Robustness by Abstract Interpretation. ACM Transactions on Programming Languages and Systems TOPLAS 46(2) Article No.: 5, Pages 1 - 31, 2024.
• Marco Campion, M. Dalla Preda, R. Giacobazzi, and C. Urban. Monotonicity and the Precision of Program Analysis. POPL2024, Volume 8, Issue POPL, Article No.: 55, Pages 1629 - 1662, London Dec. 16—20, 2024.

2023

• M. Campion, C. Urban, M. Dalla Preda, R. Giacobazzi. A Formal Framework to Measure the Incompleteness of Abstract Interpretations. SAS 2023, LNCS 14284:114-138. Cascais October 22-24, 2023.
• R. Giacobazzi, I. Mastroeni, and E. Perantoni. How Fitting is Your Abstract Domain? SAS 2023, LNCS 14284: 286-309. Cascais October 22-24, 2023.
• R. Bruni, R. Giacobazzi, R. Gori, F. Ranzato. A Correctness/Incorrectness Program Logic. Journal of the ACM 70(2): 15:1-15:45 (2023). 

2022

• R. Bruni, R. Giacobazzi, R. Gori, F. Ranzato. Abstract Interpretation Repair. 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2022). Mon 13 - Fri 17 June 2022. San Diego, California, United States.
• R. Giacobazzi and F. Ranzato. History of Abstract Interpretation. IEEE Annals of the History of Computing. IEEE Computer Society. Volume: 44, Issue: 2, 2022.
• M. Campion, M. Dalla Preda and R. Giacobazzi. Partial (In)Completeness in Abstract Interpretation: Limiting the Imprecision in Program Analysis. The 49th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2022), Sun 16 - Sat 22 January 2022, Philadelphia, Pennsylvania, United States.. Proc. ACM Program. Lang. 6, POPL, Article 59 (January 2022), 31 pages.

Current active grant: 
Started: Sept 2023

Project name: ODIN 
Title: ABSTRACT INTERPRETATION DRIVEN PROGRAMMING LANGUAGES
Funded by: AFOSR -- AIR FORCE OFFICE OF SCIENTIFIC RESEARCH
Duration: 5 years
Amount: $839,740

Abstract: Modern software industry extensively utilizes third-party code and code generated through au- tomation. How can we trust the code we use? The so-called generative artificial intelligence, based on large language models, already produces “almost correct” code, but almost is not enough. Raising our confidence significantly can only be achieved through scalable and effective program analysis. The state-of-the-art of trustworthy program design combines the Code with a proof of its correctness Analysis(Code), often specified by an abstract interpreter, i.e., Program = Code + Analysis(Code). This has some drawbacks: (1) Static program analysis reports false alarms and, like any alarm system, the fewer the false alarms, the more credible is the analysis. (2) The precision of program analysis depends upon the way the code is written. Therefore, effective program analyses and abstract inter- preters are code-driven, but tailor the analyzer to the code is extremely complex and expensive. We reverse the approach: Choose the analysis beforehand and then structure the code in a manner that is compliant for that particular analysis. Compliant here means with the minimum of false alarms. ODIN’s ambition is to lay the foundation of a new discipline of programming where the code can be efficiently and precisely verified by simpler analyzers: Program = Code(Analysis) + Analysis. Compliance of code wrt program analysis is a new, largely unexplored, frontier of program- ming that will provide the key technological advantage to make program analysis more widely used. ODIN will pioneer the research in fundamental aspects of programming languages: The interplay be- tween semantics and analysis, the nature of false-alarms, how to isolate Domain Specific Languages (DSL) compliant with an analysis, how their expressivity changes when the analysis changes, how to bound the imprecision of the analysis, and which methods and operations can be used to build verifiable code within these DSL.