ODIN addresses the challenge of ensuring the trustworthiness of code by developing scalable and effective program analysis. The current state-of-the-art approach combines code with an analysis of its correctness, often using an abstract interpreter. However, this has drawbacks: Static program analysis can generate false alarms, and fewer false alarms increase the credibility of the analysis.
Moreover, the precision of the analysis depends on how the code is written, making tailoring the analyzer to the code complex and expensive. ODIN proposes a reversed approach: selecting the analysis first and then structuring the code to comply with that analysis, minimizing false alarms. This approach involves exploring code compliance with program analysis, a relatively unexplored area and aims to make program analysis more widely used by ensuring code is written in a way that facilitates verification.
Project in cooperation with Professor Roberto Giacobazzi, at the University of Arizona (https://www.cs.arizona.edu/) .
