TY - GEN
T1 - GPU Acceleration of Bounded Model Checking with ParaFROST
AU - Osama, Muhammad
AU - Wijs, Anton
PY - 2021
Y1 - 2021
N2 - The effective parallelisation of Bounded Model Checking is challenging, due to SAT and SMT solving being hard to parallelise. We present ParaFROST, which is the first tool to employ a graphics processor to accelerate BMC, in particular the simplification of SAT formulas before and repeatedly during the solving, known as pre- and inprocessing. The solving itself is performed by a single CPU thread. We explain the design of the tool, the data structures, and the memory management, the latter having been particularly designed to handle SAT formulas typically generated for BMC, i.e., that are large, with many redundant variables. Furthermore, the solver can make multiple decisions simultaneously. We discuss experimental results, having applied ParaFROST on programs from the Core C99 package of Amazon Web Services.
AB - The effective parallelisation of Bounded Model Checking is challenging, due to SAT and SMT solving being hard to parallelise. We present ParaFROST, which is the first tool to employ a graphics processor to accelerate BMC, in particular the simplification of SAT formulas before and repeatedly during the solving, known as pre- and inprocessing. The solving itself is performed by a single CPU thread. We explain the design of the tool, the data structures, and the memory management, the latter having been particularly designed to handle SAT formulas typically generated for BMC, i.e., that are large, with many redundant variables. Furthermore, the solver can make multiple decisions simultaneously. We discuss experimental results, having applied ParaFROST on programs from the Core C99 package of Amazon Web Services.
KW - Bounded model checking
KW - GPU computing
KW - SAT solving
UR - http://www.scopus.com/inward/record.url?scp=85115873679&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-81688-9_21
DO - 10.1007/978-3-030-81688-9_21
M3 - Conference contribution
AN - SCOPUS:85115873679
SN - 9783030816872
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 447
EP - 460
BT - Computer Aided Verification - 33rd International Conference, CAV 2021, Proceedings
A2 - Silva, Alexandra
A2 - Leino, K. Rustan
PB - Springer
T2 - 33rd International Conference on Computer Aided Verification, CAV 2021
Y2 - 20 July 2021 through 23 July 2021
ER -