Automatically Identifying Soundness and Completeness Errors in Program Analysis Tools
Decanato - Facoltà di scienze informatiche
Data: 27 Settembre 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
