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
@incollection{springerlink:10.1007/978-3-642-31759-0_8,
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},
isbn={978-3-642-31758-3},
keyword={Computer Science},
pages={80-97},
volume={7385},
url={http://dx.doi.org/10.1007/978-3-642-31759-0_8},
note={10.1007/978-3-642-31759-0_8},
year={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
