Computing Colloquium Student Presentation featuring Kenny Ballou

Exploiting Incrementality in Data-Flow Analysis to Reason About Weakly-Relational Abstract Domains

Presenter: Kenny Ballou
Computing PhD Student, Computer Science emphasis

Location: In person in CCP 259 or register to attend via Zoom

Abstract: Developing correct, defect-free software for safety-critical systems is an important goal of software engineering. Verification techniques like testing and code review are adequate for certain software domains. However, they are insufficient for safety-critical software systems because these techniques cannot prove the absence of bugs for all possible execution traces. Static program analysis, on the other hand, reasons about all possible execution traces, hence, it can prove the absence of bugs. For many safety-critical systems, correctness requires the absence of numerical errors. However, verifying these numerical invariants can require expensive and complex numerical abstract domains.

Work on improving the efficiency and efficacy of weakly-relational abstract domains is presented. Specifically, work on improving efficiency of transitive closures is presented for the Zones domain, which demonstrated significant improvements to runtime of analyses. Additionally, work for incrementally identifying minimal changed variables within a Zone abstract domain is presented. Furthermore, using the minimal changed variables, a minimal union algorithm for generally comparing weakly-relational abstract domains is presented.

The presentation concludes with a preview of current work extending the presented work to the Octagons weakly-relational abstract domain, as well, as previews for longer term research building from the presented works.