Publications

• SMT Theory Arbitrage: Approximating Unbounded Constraints using Bounded Theories
  Benjamin Mikek and Qirun Zhang
  Proceedings of the 45th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2024).
• Speeding up SMT Solving via Compiler Optimization
  Benjamin Mikek and Qirun Zhang
  Proceedings of the 31st ACM Symposium on the Foundations of Software Engineering (ESEC/FSE 2023). ACM SIGSOFT Distinguished Paper Award.

Workshop Papers and Posters

• 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, Agusta, 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.