IMDEA Software

IMDEA initiative

Home > Events > Software Seminar Series > 2023 > Deciding program properties via complete abstractions on bounded domains

Nicolas Manini

Tuesday, July 4, 2023

11:00am 302-Mountain View and Zoom3 (https://zoom.us/j/3911012202, password: @s3)

Nicolas Manini, PhD Student, IMDEA Software Institute

Deciding program properties via complete abstractions on bounded domains

Abstract:

Abstract interpretation provides an over-approximation of program behaviours that is used to prove the absence of bugs. The ideal scenario for abstract interpretation is that of a complete analysis, where false alarms cannot arise. Unfortunately for any non-trivial abstract domain there is some program whose analysis is incomplete. In this talk we discuss an approach to characterizing classes of complete programs on some non-trivial abstract domains for studying their expressiveness. To this aim we present the notion of bounded domains and show the implications arising from the possibility of conducting a complete analysis on such domains. In the talk we show how to tackle the problems of deciding program termination and equivalence, and discuss applicability of our approach.