event

PhD Proposal by Benjamin Mikek

Primary tabs

Title: Towards Compiler-Guided Static Analysis

Date: Thursday, 4 December 2025

Time: 3:00-5:00 PM

Location: KACB 3100, and virtually on Zoom (https://gatech.zoom.us/j/3935457800)

 

Benjamin Mikek

Ph.D. Student

School of Computer Science

Georgia Institute of Technology

https://mikekben.github.io/

 

Committee members

Dr. Qirun Zhang (advisor): School of Computer Science, Georgia Institute of Technology

Dr. Vijay Ganesh: School of Computer Science, Georgia Institute of Technology

Dr. Jacob Laurel: School of Computer Science, Georgia Institute of Technology

Dr. Brendan Saltaformaggio: School of Cybersecurity and Privacy & School of Computer Science, Georgia Institute of Technology

 

Abstract

Static analysis consists of a large body of tools that analyze programs without running them; it is useful for checking whether programs are equivalent, for finding or proving the absence of bugs, and for verifying the security properties of software. Despite substantial progress in recent years, both theoretical and practical, existing static analyses still face major bottlenecks, including, inter alia, SMT solving, equivalence checking, and compiler verification. This work proposes a new perspective on alleviating these bottlenecks: harnessing existing compilers. It asks whether compilers' internal state, feedback mechanisms, and transformation passes can inform static analyses, improving performance and expanding the set of tractable problems. In existing work on SMT solving, we find that the strategy is promising by showing that optimizations harnessed from existing compilers can speed up SMT constraint solving. In ongoing work on translation validation, we find that a compiler's internal state can be extracted and harnessed to guide the alignment of transformed programs for translation validation. And, for future work, we propose to generalize and extend the same methodology to the task of compiler testing and verification, both by generating targeted input programs and by verifying properties of compiler components.

Status

  • Workflow status: Published
  • Created by: Tatianna Richardson
  • Created: 11/30/2025
  • Modified By: Tatianna Richardson
  • Modified: 11/30/2025

Categories

Keywords

Target Audience