Curriculum
Computer science for societal challenges and innovation, XXXIII series
Grant sponsor
FBK
Supervisor

Francesco Ranzato
Co-supervisors
Massimo Nucci

Project description
"Program testing can be used very effectively to show the presence of bugs but never to show their absence": in this famous quote, E. W. Dijkstra argues that debugging is an inadequate mean for proving correctness of programs, which can instead be formally verified through static analysis techniques. My project focuses on abstract interpretation, exploring the existence of atomic domains, and transformers for those abstractions which alter their nature, while preserving desirable properties such as algebraic and lattice structures. Domains obtained through these transformations can be combined in order to exploit emerging properties of the composition, producing new, finer abstractions. Last, I aim at automatizing this generation process by deploying machine learning techniques, systematically synthesizing abstractions which are as precise as possible for any given system. This approach offers a novel way to think and design abstract domains and, at the same time, leverages the complexity of abstract interpretation frameworks broadening its field of applicability.