2024 EuroLLVM - Leveraging LLVM Optimizations to Speed up Constraint Solving
2024 European LLVM Developers' Meeting
https://llvm.org/devmtg/2024-04/
------
Leveraging LLVM Optimizations to Speed up Constraint Solving
Speaker: Benjamin Mikek
------
Slides: https://llvm.org/devmtg/2024-04/slide...
-----
SLOT is a new tool which uses existing LLVM optimization passes to speed up SMT constraint solvers like Z3. While existing work has used SMT solving to verify LLVM’s peephole optimizations or in symbolic execution engines like KLEE, we flip the script and use LLVM optimizations to improve constraint solving. Our strategy is to translate SMT constraints into LLVM IR, apply the optimizer, and then translate back, alleviating manual developer effort in understanding both solver and LLVM internals. We find that SLOT speeds up average solving times by up to 2x for floating-point and bitvector constraints, and increases the number of constraints solved at fixed timeouts by up to 80%.
-----
Videos Edited by Bash Films: http://www.BashFilms.com
Watch video 2024 EuroLLVM - Leveraging LLVM Optimizations to Speed up Constraint Solving online without registration, duration hours minute second in high quality. This video was added by user LLVM 30 June 2024, don't forget to share it with your friends and acquaintances, it has been viewed on our site 55 once and liked it 1 people.