Employing Multiple CUDA Devices to Accelerate LTL Model Checking. - Jiri Barnat; Petr Bauch; Lubos Brim; Milan Ceska 002 (ICPADS, 2010)

CUDA Accelerated LTL Model Checking - Revisited. - Petr Bauch; Milan Ceska 002 (MEMICS, 2010)

Computing Strongly Connected Components in Parallel on CUDA. - Jiri Barnat; Petr Bauch; Lubos Brim; Milan Ceska 002 (IPDPS, 2011)

Computing Optimal Cycle Mean in Parallel on CUDA - Jiri Barnat; Petr Bauch; Lubos Brim; Milan Ceska 002 (PDMC, 2011)

Checking Sanity of Software Requirements. - Jiri Barnat; Petr Bauch; Lubos Brim (SEFM, 2012)

Designing fast LTL model checking algorithms for many-core GPUs. - Jiri Barnat; Petr Bauch; Lubos Brim; Milan Ceska 002 (J. Parallel Distributed Comput., 2012)

Control Explicit—Data Symbolic Model Checking: An Introduction - Jiri Barnat; Petr Bauch (CoRR, 2013)

Temporal Verification of Simulink Diagrams. - Jiri Barnat; Petr Bauch; Vojtech Havel (HASE, 2014)

LTL Model Checking of LLVM Bitcode with Symbolic Data. - Petr Bauch; Vojtech Havel; Jiri Barnat (MEMICS, 2014)

Model Checking Parallel Programs with Inputs. - Jiri Barnat; Petr Bauch; Vojtech Havel (PDP, 2014)

Analysing Sanity of Requirements for Avionics Systems (Preliminary Version). - Jiri Barnat; Petr Bauch; Nikola Benes; Lubos Brim; Jan Beran; Tomas Kratochvila (CoRR, 2015)

SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration. - Jan Mrázek; Petr Bauch; Henrich Lauko; Jiri Barnat (SPIN, 2016)

Analysing sanity of requirements for avionics systems. - Jiri Barnat; Petr Bauch; Nikola Benes; Lubos Brim; Jan Beran; Tomas Kratochvila (Formal Aspects Comput., 2016)

Accelerating temporal verification of Simulink diagrams using satisfiability modulo theories. - Petr Bauch; Vojtech Havel; Jiri Barnat (Softw. Qual. J., 2016)

Control Explicit-Data Symbolic Model Checking. - Petr Bauch; Vojtech Havel; Jiri Barnat (ACM Trans. Softw. Eng. Methodol., 2016)