On Parallel Software Verification Using Boolean Equation Systems

Investor logo
Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

ČEŠKA Milan DITTER Alexander LUTTGEN Gerald

Year of publication 2012
Type Article in Proceedings
Conference SPIN Workshop on Model Checking of Software
MU Faculty or unit

Faculty of Informatics

Citation
Web http://dx.doi.org/10.1007/978-3-642-31759-0_8
Doi http://dx.doi.org/10.1007/978-3-642-31759-0_8
Field Informatics
Keywords formal verification parallel model checking boolean equation systems
Description Multi- and many-core hardware platforms are today widely accessible and used to significantly accelerate many computationally de- manding 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 par- allel 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.