On Parallel Software Verification using Boolean Equation Systems

Alexander Ditter, Milan Ceska, Gerald Luttgen
University of Bamberg, 96045 Bamberg, Germany
Model Checking Software, Lecture Notes in Computer Science, Volume 7385/2012, 80-97, 2012


   author={Ditter, Alexander and Ceska, Milan and Luttgen, Gerald},

   affiliation={University of Bamberg, 96045 Bamberg, Germany},

   title={On Parallel Software Verification Using Boolean Equation Systems},

   booktitle={Model Checking Software},

   series={Lecture Notes in Computer Science},

   editor={Donaldson, Alastair and Parker, David},

   publisher={Springer Berlin / Heidelberg},


   keyword={Computer Science},







Download Download (PDF)   View View   Source Source   



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.
No votes yet.
Please wait...

* * *

* * *

HGPU group © 2010-2021 hgpu.org

All rights belong to the respective authors

Contact us: