Главная

Luboš Brim

  1. Computing Optimal Cycle Mean in Parallel on CUDA.

    Пт, 11/04/2011 - 15:01 — SomNambul
    Authors: Jiří Barnat, Luboš Brim, Milan Češka, Petr Bauch
    Subjects: and Cluster Computing, Distributed, Parallel
    Abstract

    Computation of optimal cycle mean in a directed weighted graph has many
    applications in program analysis, performance verification in particular. In
    this paper we propose a data-parallel algorithmic solution to the problem and
    show how the computation of optimal cycle mean can be efficiently accelerated
    by means of CUDA technology. We show how the problem of computation of optimal
    cycle mean is decomposed into a sequence of data-parallel graph computation
    primitives and show how these primitives can be implemented and optimized for
    CUDA computation.

  2. DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking.

    Втр, 12/15/2009 - 16:01 — SomNambul
    Authors: Jiří Barnat, Luboš Brim, Milan Češka
    Subjects: and Cluster Computing, Distributed, Parallel
    Abstract

    In this paper we present a tool that performs CUDA accelerated LTL Model
    Checking. The tool exploits parallel algorithm MAP adjusted to the NVIDIA CUDA
    architecture in order to efficiently detect the presence of accepting cycles in
    a directed graph. Accepting cycle detection is the core algorithmic procedure
    in automata-based LTL Model Checking. We demonstrate that the tool outperforms
    non-accelerated version of the algorithm and we discuss where the limits of the
    tool are and what we intend to do in the future to avoid them.

  3. BioDiVinE: A Framework for Parallel Analysis of Biological Models.

    Ср, 10/07/2009 - 12:26 — SomNambul
    Authors: Jiří Barnat, Luboš Brim, Ivana Černá, Sven Dražan, Jana Fabriková, Jan Láník, David Šafránek, Hongwu Ma
    Subjects: and Science, Computational Engineering, Finance
    Abstract

    In this paper a novel tool BioDiVinEfor parallel analysis of biological
    models is presented. The tool allows analysis of biological models specified in
    terms of a set of chemical reactions. Chemical reactions are transformed into a
    system of multi-affine differential equations. BioDiVinE employs techniques for
    finite discrete abstraction of the continuous state space. At that level,
    parallel analysis algorithms based on model checking are provided. In the
    paper, the key tool features are described and their application is
    demonstrated by means of a case study.

Math-arch

RSS-материал