GPU Acceleration of Bounded Model Checking with ParaFROST

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

4 Citations (Scopus)


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.

Original languageEnglish
Title of host publicationComputer Aided Verification - 33rd International Conference, CAV 2021, Proceedings
EditorsAlexandra Silva, K. Rustan Leino
Number of pages14
ISBN (Print)9783030816872
Publication statusPublished - 2021
Event33rd International Conference on Computer Aided Verification, CAV 2021 - Virtual, Online
Duration: 20 Jul 202123 Jul 2021

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12760 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference33rd International Conference on Computer Aided Verification, CAV 2021
CityVirtual, Online


  • Bounded model checking
  • GPU computing
  • SAT solving


Dive into the research topics of 'GPU Acceleration of Bounded Model Checking with ParaFROST'. Together they form a unique fingerprint.

Cite this