Title: A Framework for Faster Software Verification and Better Compiler Optimizations through Symbiosis

Date: Thursday, December 12th, 2024

Time: 1:00 – 3:00 PM ET
Location: Klaus 2100
Virtual Link: Zoom (Link)

Sharjeel Khan
Ph.D. Candidate
School of Computer Science

College of Computing

Georgia Institute of Technology

Committee:
Dr. Santosh Pande (Advisor) - School of Computer Science, Georgia Institute of Technology
Dr. Vivek Sarkar - School of Computer Science, Georgia Institute of Technology
Dr. Qirun Zhang - School of Computer Science, Georgia Institute of Technology
Dr. Vijay Ganesh - School of Computer Science, Georgia Institute of Technology
Dr. Eric Feron - Computer, Electrical and Mathematical Sciences and Engineering Division, King Abdullah University of Science and Technology

Abstract:
Despite numerous advancements over the years, compilers and software verification have limitations in their abilities. Due to the conservative nature of static program analysis, compiler optimizations are restricted in their applicability and effectiveness. On the other hand, software verification takes significant time on applications of reasonable sizes and, therefore, is still intractable in most cases of real-life applications. Current approaches to optimizations need to leverage verification and vice versa. This work showcases the symbiotic relationship between compiler analyses and software verification, where each uses the other's advancements. It also proposes new analyses and techniques to leverage the symbiotic relationship more effectively.

This dissertation shows both directions of the symbiotic relationship are extremely valuable. We present a framework called VICO that converts conservative dependence or alias constraints into invariants that are verified in a demand-driven way. The verified dependence invariants lead to better auto-parallelization and loop transformations in over 75 loops and an average speedup of 14.7x on Apple M1 Pro and 6.07x on Intel Xeon E5-2660 systems. The verified alias invariants lead to better register allocation and global value numbering (GVN), resulting in decreased code size and improved execution time for Linux programs and SPEC benchmarks. Regarding verification, two significant barriers faced are procedure calls and loops. To overcome procedure calls, we first present CVFunc, a framework that leverages novel compiler analysis and reinforcement learning to speed up intraprocedural software verification tasks. Specifically, we use a bi-directional dataflow analysis to detect variables affecting the verifier constructs (such as asserts). Utilizing the variables involved in verification constructs, we propose a new analysis that facilitates inlining decisions at call sites to avoid the approximation summaries introduced by the verifier. At the verifier level, we present a reinforcement learning technique for approximations and inlining and a parallel refinement to converge the verifier’s counterexample-guided abstraction and refinement (CEGAR) process faster toward an answer. As a result, CVFunc improves verification time by an average of 13.22% with a best case of (21.9%) by solving 68 new tasks (that timed out on the state-of-the-art verifier) in 843 SV-COMP software verification challenge tasks. Lastly, we present CVLoop, a framework that uses loop transformations and array dataflow analysis to speed up loop-based software verification tasks within CPAChecker and overcome the second limitation due to loops in state-of-the-art verification engines. CVLoop first abstracts the loop nest by creating an iteration model to transform the loop into simpler form for the verifier to prove properties. Next, CVLoop runs an array dataflow analysis on the leftover loops with arrays to define possible interval values that will be used to directly prove properties or generate invariants for k-induction. In SVComp’s loop category, the combination solves 38 new verification tasks in CPAChecker and an average of 11 (maximum of 23) in other software verification tools.

In summary, this dissertation develops techniques for utilizing the symbiotic relationship between compiler analysis/optimizations and software verification. It empirically demonstrates the benefits of such an approach over several problems in SV-COMP, a suite of software verification challenge tasks.