On Parallel Software Verification Using Boolean Equation Systems

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Autoři	ČEŠKA Milan DITTER Alexander LUTTGEN Gerald
Rok publikování	2012
Druh	Článek ve sborníku
Konference	SPIN Workshop on Model Checking of Software
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
www	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
Obor	Informatika
Klíčová slova	formal verification parallel model checking boolean equation systems
Popis	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.
Související projekty:	Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů Rozsáhlé výpočetní systémy: modely, aplikace a verifikace Software Components in Embedded Systems: Development and Verification Posílení zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity