Publications

• Spatial and Temporal Decomposition for Faster Translation Validation
  Benjamin Mikek, Chathur Bommineni, Qirun Zhang, and Thomas Reps
  OOPSLA 2026.
• Agentic Code Optimization via Compiler-LLM Cooperation
  Benjamin Mikek, Danylo Vashchilenko, Bryan Lu, and Panpan Xu
  Preprint 2026: arXiv:2604.04238 [cs.LO].
• SMT Theory Arbitrage: Approximating Unbounded Constraints using Bounded Theories
  Benjamin Mikek and Qirun Zhang
  PLDI 2024.
• A Performance Verification Methodology for Resource Allocation Heuristics
  Saksham Goel, Benjamin Mikek, Jehad Hussein, Venkat Arun, Ahmed Saeed, and Aditya Akella
  Preprint 2024: 2024arXiv:2301.04205 [cs.LO].
• Speeding up SMT Solving via Compiler Optimization
  Benjamin Mikek and Qirun Zhang
  ESEC/FSE 2023. ACM SIGSOFT Distinguished Paper Award.

Workshop Papers and Posters

• Extending Code Idiom Recognition to 100k+ Patterns via the OEIS
  Matthew Davis, Benjamin Mikek
  LLVM Developers Meeting (LLVM 2026), October 2026, Santa Clara CA, USA.
  [poster]
• Towards Compiler-Guided Static Analysis
  Benjamin Mikek
  SPLASH Companion (Doctoral Symposium), October 2025, Singapore, Singapore.
  [short paper]
• Leveraging LLVM Optimizations to Speed up Constraint Solving
  Benjamin Mikek, Qirun Zhang
  LLVM European Developers Meeting (EuroLLVM 2024), April 2024, Vienna, Austria.
  [presentation][extended abstract]
• Faster SMT Solving via Constraint Transformation
  Benjamin Mikek, Qirun Zhang
  Southeast Regional Programming Languages Seminar (SERPL 2023), 14 October 2023, Augusta, GA, USA.
  [presentation][extended abstract]
• Dynamically Computing Simplicial Depth in Data Sets
  Sydney Leither, Sunaina Butler, Benjamin Mikek, and Michael Burr
  COURAGE REU Conference, 27 July 2020, Virtual, USA.
  [presentation]
• Decompositions of the Incidence Matrices of Undirected Graphs
  Benjamin Mikek and Jennifer Fowler
  Joint Mathematics Meetings (JMM 2020), 17 January 2020, Denver, CO, USA.
  [poster]

Tools

• SLOT: SMT-LLVM Optimizing Translation [Github]
  A tool to speed up SMT solving of bitvector and floating-point constraints by applying compiler optimizations.