Automatically Identifying Soundness and Completeness Errors in Program Analysis Tools

Staff - Faculty of Informatics

Date: 27 September 2022 / 10:30 - 12:00

USI Campus EST, room D1.14, Sector D

Speaker: Alexandra Bugariu, ETH Zürich

Abstract: Program analysis tools (such as static analyzers, SMT solvers, and program verifiers) are extremely important for ensuring the correctness of a large variety of software systems. Very often, these tools are assumed to be sound (i.e., do not miss errors) and complete (i.e., have a low rate of false positives), otherwise their results are not reliable. However, these assumptions do not always hold in practice. Even if their theoretical designs have been proven correct, the actual implementations can still contain issues. In this talk, we discuss the challenges of  automatically identifying soundness and completeness errors in the implementations of state-of-the-art program analysis tools and present various techniques we designed to address them. Moreover, we show that these techniques are applicable to complex, highly-optimized libraries for numerical program analysis, widely-used (MAX-)SMT and automata-based solvers, as well as to mature program verifiers.

Biography: Alexandra Bugariu received her PhD in Computer Science from ETH Zürich, Switzerland in 2022, working at the intersection of programming languages and software engineering. Before that, she completed a double degree Master program at Free University of Bozen-Bolzano, Italy and Technische Universität Kaiserslautern, Germany. In 2020 and 2021, she was selected to participate as a young researcher to the Heidelberg Laureate Forum.

Host: Prof. Natasha Sharygina

Faculties

Events
08
October
2022
08.
10.
2022

Bellinzona Research Institutes Open Day

Faculty of Biomedical Sciences

The violence we do not see

Faculty of Communication, Culture and Society, Faculty of Economics
10
October
2022
10.
10.
2022

Poeti del Novecento

Faculty of Communication, Culture and Society