David Thien, Michael Smith, Evan Johnson, Sorin Lerner, Hovav Shacham, Deian Stefan, and Fraser Brown. FaJITa: Verifying Optimizations on Just-In-Time Programs PriSC 2023