Mansur, Muhammad NumairHerrmann, Andrea2024-07-262024-07-262024https://dl.gi.de/handle/20.500.12116/44196This 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.enStatic AnalysisSoundnessPrecisionPerformanceScalabilitytoolText/Journal Article