On Parallel Software Verification using Boolean Equation Systems
University of Bamberg, 96045 Bamberg, Germany
Model Checking Software, Lecture Notes in Computer Science, Volume 7385/2012, 80-97, 2012
Multi- and many-core hardware platforms are today widely accessible and used to significantly accelerate many computationally demanding tasks. In this paper we describe a parallel approach to solve Boolean Equation Systems (BESs) in the context of model checking. We focus on the applicability of state-of-the-art, shared-memory parallel hardware – multi-core CPUs and many-core GPUs – to speed up the resolution procedure for BESs. In this setting, we experimentally show the scalability and competitiveness of our approach, compared to an optimized sequential implementation, based on a large benchmark suite containing models of software systems and protocols from industry and academia.
August 6, 2012 by hgpu