ABSTRACT INTERPRETATION DRIVEN PROGRAMMING LANGUAGES
Abstract
Modern software industry extensively utilizes third-party code and code generated through automation. 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 equals Code plus 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 interpreters 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 equals Code (Analysis) plus Analysis. Compliance of code wrt program analysis is a new, largely unexplored, frontier of programming 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 between 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.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Mar 06, 2024
- Source ID
- FA95502310544
Entities
People
- Roberto Giacobazzi
Organizations
- Air Force Office of Scientific Research
- United States Air Force
- University of Verona