Zeitschriftenartikel
Automatically Detecting and Mitigating Issues in Program Analyzers
Vorschaubild nicht verfügbar
Volltext URI
Dokumententyp
Text/Journal Article
Zusatzinformation
Datum
2024
Autor:innen
Zeitschriftentitel
ISSN der Zeitschrift
Bandtitel
Verlag
Gesellschaft für Informatik e.V.
Zusammenfassung
This dissertation tackles two major challenges that impede the incorporation of static analysis tools into software development workflows, despite their potential to detect bugs and vulnerabilities in software before deployment. The first challenge addressed is unintentional unsoundness in program analyzers, such as SMT solvers and Datalog engines, which are susceptible to undetected soundness issues that can lead to severe consequences, particularly in safety-critical software. The dissertation presents novel, publicly available techniques that detected over 55 critical soundness bugs in these tools. The second challenge is balancing soundness, precision, and performance in static analyzers, which struggle with integration into diverse development scenarios due to their inability to scale and adapt to different program sizes and resource constraints. To combat this, the dissertation introduces an approach to automatically tailor abstract interpreters to specific code and resource conditions and presents a method for horizontally scaling analysis tools in cloud-based platforms.