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
Смотрите видео 2024 EuroLLVM - Leveraging LLVM Optimizations to Speed up Constraint Solving онлайн без регистрации, длительностью часов минут секунд в хорошем качестве. Это видео добавил пользователь LLVM 30 Июнь 2024, не забудьте поделиться им ссылкой с друзьями и знакомыми, на нашем сайте его посмотрели 55 раз и оно понравилось 1 людям.