Portal de Periódicos da CAPES

GPU Acceleration of Bounded Model Checking with ParaFROST

2021; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-030-81688-9_21

1611-3349

Muhammad Osama, Anton Wijs,

Model-Driven Software Engineering Techniques

Abstract 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.