Distributed LTL Model Checking Based on Negative Cycle Detection. - Lubos Brim; Ivana Cerná; Pavel Krcál; Radek Pelánek (FSTTCS, 2001)

How to Employ Reverse Search in Distributed Single Source Shortest Paths. - Lubos Brim; Ivana Cerná; Pavel Krcál; Radek Pelánek (SOFSEM, 2001)

Distributed Explicit Bounded LTL Model Checking. - Pavel Krcál (PDMC@CAV, 2003)

Timed vs. Time-Triggered Automata. - Pavel Krcál; Leonid Mokrushin; P. S. Thiagarajan; Wang Yi 001 (CONCUR, 2004)

Decidable and Undecidable Problems in Schedulability Analysis Using Timed Automata. - Pavel Krcál; Wang Yi 001 (TACAS, 2004)

On Sampled Semantics of Timed Systems. - Pavel Krcál; Radek Pelánek (FSTTCS, 2005)

Communicating Timed Automata: The More Synchronous, the More Difficult to Verify. - Pavel Krcál; Wang Yi 001 (CAV, 2006)

Multi-processor Schedulability Analysis of Preemptive Real-Time Tasks with Variable Execution Times. - Pavel Krcál; Martin Stigge; Wang Yi 001 (FORMATS, 2007)

Sampled Universality of Timed Automata. - Parosh Aziz Abdulla; Pavel Krcál; Wang Yi 001 (FoSSaCS, 2007)

Task automata: Schedulability, decidability and undecidability. - Elena Fersman; Pavel Krcál; Paul Pettersson; Wang Yi 001 (Inf. Comput., 2007)

R-Automata. - Parosh Aziz Abdulla; Pavel Krcál; Wang Yi 001 (CONCUR, 2008)

Universality of R-automata with Value Copying. - Parosh Aziz Abdulla; Pavel Krcál; Wang Yi 001 (INFINITY, 2009)

Infinite Structures in Timed Systems. - Pavel Krcál (2009)

Sampled Semantics of Timed Automata - Parosh Aziz Abdulla; Pavel Krcál; Wang Yi 001 (Log. Methods Comput. Sci., 2010)

Scalable Analysis of Fault Trees with Dynamic Features. - Jan Krcál; Pavel Krcál (DSN, 2015)

Effective Static and Dynamic Fault Tree Analysis. - Ola Bäckström; Yuliya Butkova; Holger Hermanns; Jan Krcál; Pavel Krcál (SAFECOMP, 2016)

Various Ways to Quantify BDMPs. - Marc Bouissou; Shahid Khan 002; Joost-Pieter Katoen; Pavel Krcál (MARS@ETAPS, 2020)