ParaDiSe – Parallel & Distributed Systems Laboratory

2021

Jan Mrázek, Martin Jonáš, Jiří Barnat:
Reconfiguring metamorphic robots via smt: Is it a viable way?,
2021 ieee/rsj international conference on intelligent robots and systems (iros), 2021. [BIB] [URL]

2020

Vladimír Štill:
Automatic test generation for haskell programming assignments,
Proceedings of the 2020 acm conference on innovation and technology in computer science education (iticse ’20), june 15–19, 2020, trondheim, norway, 2020. [BIB] [URL] [paper page]

2019

Henrich Lauko, Vladimír Štill, Petr Ročkai, Jiří Barnat:
Extending DIVINE with Symbolic Verification Using SMT,
Tools and algorithms for the construction and analysis of systems, 2019. [BIB] [PDF] [URL]

Vladimír Štill, Jiří Barnat:
Local nontermination detection for parallel c++ programs,
Software engineering and formal methods, 2019. [BIB] [URL] [paper page]

Jan Mrázek, Jiří Barnat:
RoFICoM – First Open-Hardware Connector for Metamorphic Robots,
2019 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), 2019. [BIB] [PDF] [URL]

2018

Petr Ročkai, Vladimír Štill, Ivana Černá, Jiří Barnat:
DiVM: Model checking with LLVM and graph memory,
Journal of Systems and Software, 2018. [BIB] [PDF] [URL] [paper page]

Jaroslav Bendík, Nikola Beneš, Ivana Černá:
Finding regressions in projects under version control systems,
ICSOFT, 2018. [BIB]

Vladimír Štill:
Memory-Model-Aware Analysis of Parallel Programs,
Advanced Master’s thesis, 2018. [BIB] [URL]

Vladimír Štill, Jiří Barnat:
Model Checking of C++ Programs Under the x86-TSO Memory Model,
Formal methods and software engineering, 2018. [BIB] [PDF] [URL] [paper page]

Jaroslav Bendík, Elaheh Ghassabani, Michael W. Whalen, Ivana Černá:
Online enumeration of all minimal inductive validity cores,
SEFM, 2018. [BIB]

Jaroslav Bendík, Ivana Černá, Nikola Beneš:
Recursive online enumeration of all minimal unsatisfiable subsets,
ATVA, 2018. [BIB]

Henrich Lauko, Petr Ročkai, Jiří Barnat:
Symbolic computation via program transformation,
Theoretical aspects of computing – ictac 2018, 2018. [BIB] [PDF] [URL]

2017

Jaroslav Bendík:
Consistency checking in requirements analysis,
ISSTA, 2017. [BIB]

Katarína Kejstová, Petr Ročkai, Jiří Barnat:
From Model Checking to Runtime Verification and Back,
Runtime verification - 17th international conference, RV 2017, 2017. [BIB] [URL] [paper page]

Zuzana Baranová, Jiří Barnat, Katarína Kejstová, Tadeáš Kučera, Henrich Lauko, Jan Mrázek, Petr Ročkai, Vladimír Štill:
Model Checking of C and C++ with DIVINE 4,
International symposium on automated technology for verification and analysis (atva) (to appear), 2017. [BIB] [PDF] [URL] [paper page]

Jan Mrázek, Martin Jonáš, Vladimír Štill, Henrich Lauko, Jiří Barnat:
Optimizing and Caching SMT Queries in SymDIVINE,
Tools and algorithms for the construction and analysis of systems, 2017. [BIB] [URL]

Vladimír Štill, Petr Ročkai, Jiří Barnat:
Using off-the-shelf exception support components in c++ verification,
IEEE international conference on software quality, reliability and security (qrs), 2017. [BIB] [PDF] [URL] [paper page]

2016

Petr Bauch, Vojtěch Havel, Jiří Barnat:
Accelerating temporal verification of simulink diagrams using satisfiability modulo theories,
Software Quality Journal, 2016. [BIB] [URL]

Jaroslav Bendík:
Algorithms for Finding Maximal Satisfiable Sets of Constraints,
Master’s Thesis, 2016. [BIB] [PDF] [URL]

Jan Mrázek:
Caching SMT Queries in SymDIVINE,
Bachelor’s Thesis, 2016. [BIB] [PDF] [URL]

Vladimír Štill, Petr Ročkai, Jiří Barnat:
DIVINE: Explicit-State LTL Model Checker,
Tools and Algorithms for the Construction and Analysis of Systems, 2016. [BIB] [PDF] [URL]

Jaroslav Bendík, Nikola Beneš, Jiří Barnat, Ivana Černá:
Finding boundary elements in ordered sets with application to safety and requirements analysis,
Software engineering and formal methods - 14th international conference, SEFM 2016, held as part of STAF 2016, vienna, austria, july 4-8, 2016, proceedings, 2016. [BIB] [URL]

Vladimír Štill:
LLVM Transformations for Model Checking,
Master’s Thesis, 2016. [BIB] [PDF] [URL]

Peter Bezděk, Nikola Beneš, Jiří Barnat, Ivana Černá:
LTL parameter synthesis of parametric timed automata,
Software engineering and formal methods - 14th international conference, SEFM 2016, held as part of STAF 2016, vienna, austria, july 4-8, 2016, proceedings, 2016. [BIB] [URL]

Jiří Barnat, Ivana Černá, Petr Ročkai, Vladimír Štill, Kristína Zákopčanová:
On Verifying C++ Programs with Probabilities,
ACM Symposium on Applied Computing, 2016. [BIB] [URL]

Eva Tesařová:
Optimal Sensor Scheduling for Systems under Temporal Constraints,
Master’s Thesis, 2016. [BIB] [PDF] [URL]

Jan Mrázek, Petr Bauch, Henrich Lauko, Jiří Barnat:
SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration,
Model Checking Software: 23rd International Symposium, SPIN, 2016. [BIB] [PDF] [URL]

Jiří Weiser:
TCP vrstva pro verifikační nástroj DIVINE,
Diplomová práce, 2016. [BIB] [PDF] [URL]

Jaroslav Bendík, Nikola Beneš, Ivana Černá, Jiří Barnat:
Tunable online MUS/MSS enumeration,
FSTTCS, 2016. [BIB]

Vladimír Štill, Petr Ročkai, Jiří Barnat:
Weak Memory Models as LLVM-to-LLVM Transformations,
Mathematical and Engineering Methods in Computer Science, Revised Selected Papers, 2016. [BIB] [PDF] [URL]

2015

Mária Svoreňová:
Control Strategy Synthesis for Path Planning under Temporal Constraints,
Ph.D. Thesis, 2015. [BIB] [PDF] [URL]

Jiří Barnat, Petr Ročkai, Vladimír Štill, Jiří Weiser:
Fast, dynamically-sized concurrent hash table,
Model checking software (spin 2015), 2015. [BIB] [PDF] [URL]

Petr Ročkai:
Model checking software,
Ph.D. Thesis, 2015. [BIB] [PDF] [URL]

Kristína Zákopčanová:
On Chaining Divine and Prism Model Checkers,
Bachelor’s Thesis, 2015. [BIB] [PDF] [URL]

Mária Svoreňová, Ivana Černá, Calin Belta:
Optimal temporal logic control for deterministic transition systems with probabilistic penalties,
IEEE Transactions on Automatic Control, 2015. [BIB]

Jiří Barnat:
Quo vadis explicit-state model checking,
SOFSEM 2015: Theory and practice of computer science - 41st international conference on current trends in theory and practice of computer science, 2015. [BIB] [URL]

Petr Ročkai, Vladimír Štill, Jiří Barnat:
Techniques for Memory-Efficient Model Checking of C and C++ Code,
Software Engineering and Formal Methods, 2015. [BIB] [PDF] [URL]

Mária Svoreňová, Jan Křetínský, Martin Chmelík, Krishnendu Chatterjee, Ivana Černá, Calin Belta:
Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games,
Proceedings of acm international conference on hybrid systems: Computation and control, 2015. [BIB]

Mária Svoreňová, Martin Chmelík, Kevin Leahy, Hasan Ferit Eniser, Krishnendu Chatterjee, Ivana Černá, Calin Belta:
Temporal logic motion planning using pomdps with parity objectives,
Proceedings of acm international conference on hybrid systems: Computation and control, 2015. [BIB]

Milan Lenčo:
Verification of Name Service Cache Daemon with DIVINE Model Checker,
Master’s Thesis, 2015. [BIB] [PDF] [URL]

2014

Vladimír Štill, Petr Ročkai, Jiří Barnat:
Context-Switch-Directed Verification in DIVINE,
Mathematical and Engineering Methods in Computer Science, 2014. [BIB] [PDF] [URL]

Jaroslav Bendík:
Detekce cyklů v dynamických grafech,
Bakalářská práce, 2014. [BIB] [PDF] [URL]

Vojtěch Havel:
Generic Platform for Explicit-Symbolic Verification,
Master’s Thesis, 2014. [BIB] [PDF] [URL]

Petr Bauch, Vojtěch Havel, Jiří Barnat:
LTL model checking of llvm bitcode with symbolic data,
Proceedings of memics’14, 2014. [BIB] [URL]

Peter Bezděk, Nikola Beneš, Jiří Barnat, Ivana Černá:
LTL model checking of parametric timed automata,
MEMICS 2014, 2014. [BIB]

Petr Ročkai, Jiří Barnat, Luboš Brim:
Model Checking C++ with Exceptions,
Automated verification of critical systems, 2014. [BIB] [URL]

Jiří Barnat, Petr Bauch, Vojtěch Havel:
Model Checking Parallel Programs with Inputs,
Parallel, distributed and network-based processing (pdp), 2014 22nd euromicro international conference on, 2014. [BIB] [URL]

Eva Tesařová:
Modelování systémů s reálným časem a pravděpodobností,
Bakalářská práce, 2014. [BIB] [PDF] [URL]

Peter Bezděk, Nikola Beneš, Vojtěch Havel, Jiří Barnat, Ivana Černá:
On Clock-Aware LTL properties of Timed Automata,
International colloquium on theoretical aspects of computing (ictac), 2014. [BIB]

Jiří Barnat, Petr Bauch, Vojtěch Havel:
Temporal verification of simulink diagrams,
Proceedings of hase 2014, 2014. [BIB]

Jiří Barnat, Nikola Beneš, Tomáš Bureš, Ivana Černá, Jaroslav Keznikl, František Plášil:
Towards Verification of Ensemble-Based Component Systems,
Formal aspects of component software (facs), 2014. [BIB]

2013

Jiří Barnat, Nikola Beneš, Ivana Černá, Zuzana Petruchová:
DCCL: Verification of Component Systems with Ensembles,
Proceedings of the 16th international acm sigsoft symposium on component-based software engineering, 2013. [BIB] [URL]

Jiří Barnat, Luboš Brim, Vojtěch Havel, Jan Havlíček, Jan Kriho, Milan Lenčo, Petr Ročkai, Vladimír Štill, Jiří Weiser:
DiVinE 3.0 – An Explicit-State Model Checker for Multithreaded C & C++ Programs,
Computer Aided Verification, 2013. [BIB] [URL]

Jiří Barnat, Jan Havlíček, Petr Ročkai:
Distributed ltl model checking with hash compaction,
Electronic notes in theoretical computer science, volume 296, 2013. [BIB] [URL]

Jiří Weiser:
Dynamicky rostoucí sdílená hašovací tabulka pro DiVinE,
Bakalářská práce, 2013. [BIB] [PDF] [URL]

Luboš Brim, Milan Češka, Sven Dražan, David Šafránek:
Exploring parameter space of stochastic biochemical systems using quantitative model checking,
Computer aided verification: 25th international conference, cav 2013, saint petersburg, russia, july 13-19, 2013. Proceedings, 2013. [BIB] [URL]

Boyan Yordanov, Jana Tůmová, Ivana Černá, Jiří Barnat, Calin Belta:
Formal analysis of piecewise affine systems through formula-guided refinement,
Automatica, 2013. [BIB] [URL]

Petr Ročkai, Jiří Barnat, Luboš Brim:
Improved State Space Reductions for LTL Model Checking of C & C++ Programs,
NASA Formal Methods (NFM 2013), 2013. [BIB] [URL]

Jiří Barnat, Luboš Brim, Vojtěch Havel:
LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model,
Application of Concurrency to System Design (ACSD), 2013. [BIB] [URL]

Luboš Brim, Milan Češka, David Šafránek:
Model checking of biological systems,
Formal methods for dynamical systems: 13th international school on formal methods for the design of computer, communication, and software systems, sfm 2013, bertinoro, italy, june 17-22, 2013. Advanced lectures, 2013. [BIB] [URL]

Luboš Brim, Milan Češka, Sven Dražan, David Šafránek:
On robustness analysis of stochastic biochemical systems by probabilistic model checking,
arXiv preprint arXiv:1310.4734, 2013. [BIB]

Mária Svoreňová, Ivana Černá, Calin Belta:
Optimal control of mdps with temporal logic constraints,
Proceedings of the 52nd ieee conference on decision and control, 2013. [BIB] [URL]

Mária Svoreňová, Ivana Černá, Calin Belta:
Optimal receding horizon control for finite deterministic systems with temporal logic constraints,
Proceedings of the 2013 american control conference, 2013. [BIB] [URL]

Luboš Brim, Vilém Děd, David Šafránek:
Qualitative modelling and analysis of photosystem ii,
CEUR workshop proceedings, 2013. [BIB] [URL]

Luboš Brim, Tomáš Vejpustek, David Šafránek, Jana Fabriková:
Robustness analysis for value-freezing signal temporal logic,
Proceedings hsb 2013, 2013. [BIB] [URL]

Vladimír Štill:
State Space Compression for the DiVinE Model Checker,
Bachelor’s Thesis, 2013. [BIB] [PDF] [URL]

S. Van Goethem, J. M. Jacquet, Luboš Brim, David Šafránek:
Timed modelling of gene networks with arbitrarily precise expression discretization,
Electron. Notes Theor. Comput. Sci., 2013. [BIB] [URL]

Jan Havlíček:
Untimed LTL Model Checking of Timed Automata,
Master’s Thesis, 2013. [BIB] [PDF] [URL]

2012

Mária Svoreňová, Jana Tůmová, Jiří Barnat, Ivana Černá:
Attraction-Based Receding Horizon Path Planning with Temporal Logic Constraints,
IEEE conference on decision and control (cdc 2012), 2012. [BIB]

Jiří Barnat, Petr Bauch, Luboš Brim:
Checking sanity of software requirements,
Software engineering and formal methods: 10th international conference, sefm 2012, thessaloniki, greece, october 1-5, 2012. Proceedings, 2012. [BIB] [URL]

Jiří Barnat, Petr Bauch, Luboš Brim, Milan Češka:
Designing fast ltl model checking algorithms for many-core gpus,
Journal of Parallel and Distributed Computing, 2012. [BIB] [URL]

Jiří Barnat, Luboš Brim, Jan Beran, Tomáš Kratochvíla, Italo Romani Oliveira:
Executing model checking counterexamples in simulink,
IEEE sixth international symposium on theoretical aspects of software engineering, 2012. [BIB]

Nikola Beneš, Ivana Černá, Filip Štefaňák:
Factorization for component-interaction automata,
SOFSEM 2012: Theory and practice of computer science, 2012. [BIB] [URL]

Jiří Barnat, Luboš Brim, Adam Krejci, Adam Streck, David Šafránek, Martin Vejnár, Tomáš Vejpustek:
On parameter synthesis by parallel model checking,
IEEE/ACM Trans. Comput. Biol. Bioinformatics, 2012. [BIB] [URL]

Jiří Barnat, Luboš Brim, Petr Ročkai:
On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties,
Science of Computer Programming, 2012. [BIB] [URL]

Vojtěch Havel:
Relaxed Memory Models in DiVinE,
Bachelor’s Thesis, 2012. [BIB] [PDF] [URL]

Nikola Beneš, Barbora Bühnová, Ivana Černá, Radek Ošlejšek:
Reliability analysis in component-based development via probabilistic model checking,
Proceedings of the 15th acm sigsoft symposium on component based software engineering (cbse ’12), 2012. [BIB] [URL]

Boyan Yordanov, Jana Tůmová, Ivana Černá, Jiří Barnat, Calin Belta:
Temporal logic control of discrete-time piecewise affine systems,
IEEE Transactions on Automatic Control, 2012. [BIB] [URL]

Boyan Yordanov, Jana Tůmová, Ivana Černá, Jiří Barnat, Calin Belta:
Temporal logic control of discrete-time piecewise affine systems,
IEEE Transactions on Automatic Control, 2012. [BIB] [URL]

Jiří Barnat, Ivana Černá, Jana Tůmová:
Timed automata approach to verification of systems with degradation,
MEMICS 2011, 2012. [BIB] [URL]

Jiří Barnat, Jan Beran, Luboš Brim, Kratochvíla Tomáš, Ročkai Petr:
Tool chain to support automated formal verification of avionics simulink designs,
Formal methods for industrial critical systems: 17th international workshop, fmics 2012, paris, france, august 27-28, 2012. Proceedings, 2012. [BIB] [URL]

Jiří Barnat, Luboš Brim, Petr Ročkai:
Towards ltl model checking of unmodified thread-based c & c++ programs,
NASA formal methods: 4th international symposium, nfm 2012, norfolk, va, usa, april 3-5, 2012. Proceedings, 2012. [BIB] [URL]

Jiří Barnat, Ivana Černá, Jana Tůmová:
Verification of systems with degradation,
Computing and Informatics, 2012. [BIB]

2011

Pieter Collins, Luc Habets, Jan Schuppen, Ivana Černá, Jana Fabriková, David Šafránek:
Abstraction of biochemical reaction systems on polytopes,
Proceedings of the 18th ifac world congress, 2011. [BIB] [URL]

Nikola Beneš, Ivana Černá, Milan Křivánek:
CoInDiVinE: Parallel distributed model checker for component-based systems,
Proceedings 10th international workshop on parallel and distributed methods in verifiCation, 2011. [BIB] [URL]

Jiří Barnat, Petr Bauch, Luboš Brim, Milan Češka:
Computing optimal cycle mean in parallel on cuda,
Electronic Proceedings in Theoretical Computer Science, 2011. [BIB] [URL] [paper page]

Jiří Barnat, Petr Bauch, Luboš Brim, Milan Ceška:
Computing strongly connected components in parallel on cuda,
Parallel distributed processing symposium (ipdps), 2011 ieee international, 2011. [BIB] [URL]

Jiří Barnat, Jakub Chaloupka, Jaco Pol:
Distributed algorithms for scc decomposition,
Journal of Logic and Computation, 2011. [BIB] [URL]

Stefan Edelkamp, Damian Sulewski, Jiří Barnat, Luboš Brim, Pavel Šimeček:
Flash memory efficient ltl model checking,
Science of Computer Programming, 2011. [BIB] [URL]

Nikola Beneš, Ivana Černá, Jan Křetínský:
Modal transition systems: Composition and ltl model checking,
ATVA 2011 - automated technology for verification and analysis: 9th international symposium, 2011. [BIB]

Nikola Beneš, Luboš Brim, Barbora Bühnová, Ivana Černá, Jiří Sochor, Pavlína Moravcová Vařeková:
Partial order reduction for state/event ltl with application to component-interaction automata,
Science of Computer Programming, 2011. [BIB] [URL]

Luboš Brim, Jiří Barnat:
Platform dependent verification: On engineering verification tools for 21st century,
Electronic Proceedings in Theoretical Computer Science, 2011. [BIB] [URL] [paper page]

Luboš Brim, Jana Fabriková, Sven Dražan, David Šafránek:
Reachability in biochemical dynamical systems by quantitative discrete approximation,
Electronic Proceedings in Theoretical Computer Science, 2011. [BIB] [URL]

Roman Plášil:
Vysvětlování protipříkladů v nástroji divine [online],
Master’s Thesis, 2011. [BIB] [URL]

2010

Jana Tůmová, Boyan Yordanov, Calin Belta, Ivana Černá, Jiří Barnat:
A symbolic approach to controlling piecewise affine systems,
Proceedings of of the 49th ieee conference on decision and control (cdc), 2010. [BIB]

Jiří Barnat, Luboš Brim, Milan Češka, Petr Ročkai:
DiVinE: Parallel Distributed Model Checker,
Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology, 2010. [BIB] [URL]

Jiří Barnat, Jakub Chaloupka, Jaco Pol:
Distributed Algorithms for SCC Decomposition,
Journal of Logic and Computation, 2010. [BIB] [URL]

Jiří Barnat, Petr Bauch, Luboš Brim, Milan Češka:
Employing Multiple CUDA Devices to Accelerate LTL Model Checking,
16th International Conference on Parallel and Distributed Systems (ICPADS 2010), 2010. [BIB]

Boyan Yordanov, Jana Tůmová, Calin Belta, Ivana Černá, Jiří Barnat:
Formal analysis of piecewise affine systems through formula -guided refinement,
Proceedings of of the 49th ieee conference on decision and control (cdc), 2010. [BIB]

Jiří Barnat, Luboš Brim, David Šafránek:
High-Performance Analysis of Biological Systems Dynamics with the DiVinE Model Checker,
Briefings in Bioinformatics, 2010. [BIB] [URL]

Jiří Barnat, Luboš Brim, Petr Ročkai:
Parallel Partial Order Reduction with Topological Sort Proviso,
Proceeding of SEFM 2010, 2010. [BIB]

Jiří Barnat, Luboš Brim, David Šafránek, Martin Vejnár:
Parameter Scanning by Parallel Model Checking with Applications in Systems Biology,
Proceedings of joint HiBi/PDMC workshop (HiBi/PDMC 2010), 2010. [BIB]

Petr Ročkai:
Partial Order Reduction in Parallel Model Checking,
Master’s Thesis, 2010. [BIB] [PDF] [URL]

Jiří Barnat, Luboš Brim, Petr Ročkai:
Scalable Shared Memory LTL Model Checking,
International Journal on Software Tools for Technology Transfer (STTT), 2010. [BIB] [URL]

Mária Svoreňová:
Verifikace hybridních systémů,
Bakalářská práce, 2010. [BIB] [PDF] [URL]

2009

Jiří Barnat, Luboš Brim, Petr Ročkai:
A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties,
Formal methods and software engineering (icfem 2009), 2009. [BIB]

Jiří Barnat, Luboš Brim, Ivana Černá, Sven Dražan, Jana Fabriková, Jan Láník, David Šafránek, Hongwu Ma:
BioDiVinE: A Framework for Parallel Analysis of Biological Models,
Electronic Proceedings in Theoretical Computer Science (COMPMOD 2009), 2009. [BIB] [URL]

Jiří Barnat, Luboš Brim, Ivana Černá, Sven Dražan, Jana Fabriková, Jan Láník, David Šafránek:
BioDiVinE: A Tool for Parallel Analysis of Multi-Affine ODE Models,
Proceedings of the 7th conference on computational methods in systems biology (cmsb’09), 2009. [BIB]

Jiří Barnat, Luboš Brim, Milan Češka, Tomáš Lamr:
CUDA accelerated LTL Model Checking,
15th international conference on parallel and distributed systems (icpads 2009), 2009. [BIB]

Jiří Barnat, Luboš Brim, Pavel Šimeček:
Cluster-Based I/O Efficient LTL Model Checking,
24th ieee/acm international conference on automated software engineering (ase 2009), 2009. [BIB]

Jiří Barnat, Luboš Brim, Ivana Černá, Sven Dražan, Jana Fabriková, David Šafránek:
Computational Analysis of Large-Scale Multi-Affine ODE Models,
2009 international workshop on high performance computational systems biology (hibi 2009), 2009. [BIB]

Jiří Barnat, Luboš Brim, Petr Ročkai:
DiVinE 2.0: High-Performance Model Checking,
2009 international workshop on high performance computational systems biology (hibi 2009), 2009. [BIB]

Jiří Barnat, Luboš Brim, Milan Češka:
DiVinE-CUDA: A Tool for GPU Accelerated LTL Model Checking,
Electronic Proceedings in Theoretical Computer Science (PDMC 2009), 2009. [BIB] [URL]

Kees Verstoep, Henri Bal, Jiří Barnat, Luboš Brim:
Efficient Large-Scale Model Checking,
23rd ieee international parallel & distributed processing symposium (ipdps 2009), 2009. [BIB]

Radek Pelánek:
Fighting state space explosion: Review and evaluation,
Formal methods for industrial critical systems: 13th international workshop, fmics 2008, l’Aquila, italy, september 15-16, 2008, revised selected papers, 2009. [BIB] [URL]

Jiří Barnat, Luboš Brim, Ivana Černá, Milan Češka, Jana Tůmová:
Local quantitative ltl model checking,
Formal methods for industrial critical systems, 2009. [BIB] [URL]

Jiří Barnat, Luboš Brim, Ivana Černá, Sven Dražan, Jana Fabriková, David Šafránek:
On algorithmic analysis of transcriptional regulation by LTL model checking,
Theor. Comput. Sci., 2009. [BIB] [URL]

Laura Bozzelli, Mojmír Křetínský, Vojtěch Řehák, Jan Strejček:
On decidability of ltl model checking for process rewrite systems,
Acta informatica, 2009. [BIB] [URL] [paper page]

Nikola Beneš, Luboš Brim, Ivana Černá, Jiří Sochor, Pavlína Vařeková, Barbora Zimmerová:
Partial Order Reduction for State/Event LTL,
Proceedings of the international conference on integrated formal methods (ifm’09), 2009. [BIB] [paper page]

Jiří Barnat, Ivana Černá, Jana Tůmová:
Quantitative Model Checking of Systems with Degradation,
Proceeding of the sixth international conference on quantitative evaluation of systems (qest 2009), 2009. [BIB]

2008

Nikola Beneš, Ivana Černá, Jiří Sochor, Pavlína Vařeková, Barbora Zimmerová:
A case study in parallel verification of component-based systems,
Electr. Notes Theor. Comput. Sci., 2008. [BIB] [URL]

Pavlína Vařeková, Ivana Černá:
Automated computing of the maximal number of handled clients for client-server systems,
Proceedings of facs’08, 2008. [BIB]

Jiří Barnat, Luboš Brim, Stefan Edelkamp, Damian Sulewski, Pavel Šimeček:
Can Flash Memory Help in Model Checking,
Formal methods for industrial critical systems (fmics 2008), 2008. [BIB]

Jiří Barnat, Luboš Brim, Petr Ročkai:
DiVinE Multi-Core – A Parallel LTL Model-Checker,
Automated technology for verification and analysis (atva 2008), 2008. [BIB]

Pavlína Vařeková, Barbora Zimmerová, Pavel Moravec, Ivana Černá:
Formal Verification of Systems with an Unlimited Number of Components,
IET Software journal, 2008. [BIB]

Jiří Barnat, Luboš Brim, Ivana Černá, Sven Dražan, David Šafránek:
From simple regulatory motifs to parallel model checking of complex transcriptional networks,
Proceedings of pdmc 2008 - parallel and distributed methods ins verification, 2008. [BIB]

Jiří Barnat, Jakub Chaloupka, Jaco Pol:
Improved Distributed Algorithms for SCC Decomposition,
ENTCS, 2008. [BIB]

Jiří Barnat, Jakub Chaloupka, Jaco Pol:
Improved distributed algorithms for scc decomposition,
Electronic Notes in Theoretical Computer Science, 2008. [BIB] [URL]

Jiří Barnat, Luboš Brim, Ivana Černá, Milan Češka, Jana Tůmová:
Local Quantitative LTL Model Checking,
Formal methods for industrial critical systems (fmics 2008), 2008. [BIB]

Pavlína Vařeková, Ivana Černá:
Model checking of control-user component-based parametrised systems,
CBSE’08, 2008. [BIB]

Radek Pelánek:
Model classifications and automated verification,
Formal methods for industrial critical systems: 12th international workshop, fmics 2007, berlin, germany, july 1-2, 2007, revised selected papers, 2008. [BIB] [URL]

Petr Ročkai:
Multi-Threaded Nested DFS,
Bachelor’s Thesis, 2008. [BIB] [PDF] [URL]

Jiří Barnat, Luboš Brim, Ivana Černá, Sven Dražan, David Šafránek:
Parallel Model Checking Large-Scale Genetic Regulatory Networks with DiVinE,
ENTCS, 2008. [BIB]

Jiří Barnat, Luboš Brim, Ivana Černá, Milan Češka, Jana Tůmová:
ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems,
QEST ’08: Proceedings of the 2008 fifth international conference on quantitative evaluation of systems, 2008. [BIB] [URL]

Jiří Barnat, Luboš Brim, Pavel Šimeček, Michael Weber:
Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking,
Tools and algorithms for the construction and analysis of systems (tacas)., 2008. [BIB]

Stefan Edelkamp, Peter Sanders, Pavel Šimeček:
Semi-external ltl model checking,
20th international conference on computer aided verification, 2008. [BIB]

Jiří Barnat, Petr Ročkai:
Shared Hash Tables in Parallel Model Checking,
ENTCS, 2008. [BIB]

Luboš Brim, Jiří Barnat:
Squeeze All the Power Out of Your Hardware to Verify Your Software!,
ISOLA 2008, 2008. [BIB]

Nikola Beneš, Luboš Brim, Ivana Černá, Jiří Sochor, Pavlína Vařeková, Barbora Zimmerová:
The CoIn Tool: Modelling and Verification of Interactions in Component-Based Systems,
Proceedings of the workshop on formal aspects of component software (facs’08), 2008. [BIB]

Barbora Zimmerová, Pavlína Vařeková, Nikola Beneš, Ivana Černá, Luboš Brim, Jiří Sochor:
The Common Component Modeling Example: Comparing Software Component Models,
2008. [BIB]

2007

Radek Pelánek:
BEEM: Benchmarks for explicit model checkers,
Model checking software, 2007. [BIB] [URL]

Pavelína Vařeková, Barbora Zimmerová:
Challenge problem: Subject-observer specification with component-interaction automata,
Proceedings of the 2007 conference on specification and verification of component-based systems: 6th joint meeting of the european conference on software engineering and the acm sigsoft symposium on the foundations of software engineering, 2007. [BIB]

Ivana Černá, Pavlína Vařeková, Barbora Zimmerová:
Component Substitutability via Equivalencies of Component-Interaction Automata,
Electronic Notes in Theoretical Computer Science, 2007. [BIB] [URL] [paper page]

Luboš Brim:
Distributed verification: Exploring the power of raw computing power,
Formal methods: Applications and technology: 11th international workshop, fmics 2006 and 5th international workshop pdmc 2006, bonn, germany, august 26-27, and august 31, 2006, revised selected papers, 2007. [BIB] [URL]

Pavlína Vařeková, Pavel Moravec, Ivana Černá, Barbora Zimmerová:
Effective Verification of Systems with a Dynamic Number of Components,
Proceedings of the esec/fse conference on specification and verification of component-based systems (savcbs’07), 2007. [BIB] [URL]

Jiří Barnat, Luboš Brim, Pavel Šimeček:
I/O Efficient Accepting Cycle Detection,
Computer aided verification, 2007. [BIB]

Luboš Brim, Mojmír Křetínský:
Model checking large finite-state systems and beyond,
33rd conference on current trends in theory and practice of computer science, 2007. [BIB]

Luboš Brim, Ivana Černá, Pavel Moravec, Jiří Šimša:
On combining partial order reduction with fairness assumptions,
FMICS/pdmc, 2007. [BIB]

Ahmed Bouajjani, Jan Strejček, Tayssir Touili:
On symbolic verification of weakly extended pad,
Proceedings of the 13th international workshop on expressiveness in concurrency (express 2006), 2007. [BIB] [URL]

Jiří Barnat, Luboš Brim, Martin Leucker:
Parallel Model Checking and the FMICS-jETI Platform,
The twelfth ieee international conference on engineering of complex computer systems (iceccs 2007), 2007. [BIB]

Jiří Barnat, Luboš Brim, Ivana Černá, Sven Dražan, David Šafránek:
Parallel model-checking genetic regulatory networks,
Towards systems biology, 2007. [BIB]

Jiří Barnat, Luboš Brim, Ivana Černá, Milan Češka, Jana Tůmová:
ProbDiVinE: A Parallel Qualitative LTL Model Checker,
Fourth International Conference on the Quantitative Evaluation of Systems (QEST’07), 2007. [BIB]

Jiří Barnat, Luboš Brim, Petr Ročkai:
Scalable multi-core ltl model-checking,
Model checking software, 2007. [BIB]

Luboš Brim, Jiří Barnat:
Tutorial: Parallel model checking,
Model checking software, 2007. [BIB]

2006

Jiří Barnat, Luboš Brim, Ivana Černá:
Cluster-based ltl model checking of large systems,
Formal methods for components and objects, 2006. [BIB]

Ivana Černá, Pavlína Vařeková, Barbora Zimmerová:
Component substitutability via equivalencies of component-interaction automata,
Pre-proceedings of the international workshop on formal aspects of component software (facs’06), 2006. [BIB]

Radek Pelánek, Jan Strejček:
Deeper connections between ltl and alternating automata,
Implementation and application of automata: 10th international conference, ciaa 2005, sophia antipolis, france, june 27-29, 2005, revised selected papers, 2006. [BIB] [URL]

Jiří Barnat, Luboš Brim, Ivana Černá, Pavel Moravec, Petr Ročkai, Pavel Šimeček:
DiVinE – A Tool for Distributed Verification (Tool Paper),
Computer Aided Verification, 2006. [BIB]

Jiří Barnat, Ivana Černá:
Distributed Breadth-First Search LTL Model Checking,
Special Issue on Parallel and Distributed Databases of Formal Methods in System Design, 2006. [BIB]

Ivana Černá, Tomáš Brázdil:
Model checking of regctl,
Computing and Informatics, 2006. [BIB]

Jiří Šimša:
Monitorování chování systémů,
Master’s Thesis, 2006. [BIB] [PDF] [URL]

Laura Bozzelli, Mojmír Křetínský, Vojtěch Řehák, Jan Strejček:
On decidability of ltl model checking for process rewrite systems,
FSTTCS 2006: 26th international conference on foundations of software technology and theoretical computer science, 26th international conference, kolkata, india, december 13-15, 2006, proceedings, 2006. [BIB] [paper page]

Jiří Barnat, Pavel Moravec:
Parallel Algorithms for Finding SCCs in Implicitly Given Graphs,
Formal methods: Applications and technology, 2006. [BIB]

2005

Jiří Barnat, Luboš Brim, Ivana Černá:
Cluster-Based LTL Model Checking of Large Systems,
Formal Methods for Components and Objects, 2005. [BIB]

Barbora Zimmerová, Luboš Brim, Ivana Černá, Pavlína Vařeková:
Component-Interaction Automata as a Verification-Oriented Component-Based System Specification,
Specification and verification of component-based systems (savcbs 05), 2005. [BIB]

Jiří Barnat, Luboš Brim, Ivana Černá, Pavel Šimeček:
DiVinE – The Distributed Verification Environment,
Proceedings of 4th international workshop on parallel and distributed methods in verifiCation, 2005. [BIB]

Luboš Brim, Ivana Černá, Pavel Moravec, Jiří Šimša:
Distributed Partial Order Reduction,
Electronic Notes in Theoretical Computer Science, 2005. [BIB]

Jiří Barnat, Vojěch Forejt, Martin Leucker, Michael Weber:
DivSPIN – A SPIN compatible distributed model checker,
Proceedings of 4th international workshop on parallel and distributed methods in verifiCation, 2005. [BIB]

Radek Pelánek, Tomáš Hanžl, Ivana Černá, Luboš Brim:
Enhancing Random Walk State Space Exploration,
Tenth international workshop on formal methods for industrial critical systems (fmics 05), 2005. [BIB]

Jiří Barnat, Luboš Brim, Jakub Chaloupka:
From Distributed Memory Cycle Detection to Parallel LTL Model Checking,
Electronic Notes in Theoretical Computer Science, 2005. [BIB]

Pavel Moravec:
How to cope with higher dependency in partial order reduction for ltl model checking,
1st doctoral workshop on mathematical and engineering methods in computer science (memics 2005), 2005. [BIB] [URL]

Luboš Brim, Ivana Černá, Pavel Moravec, Jiří Šimša:
How to order vertices for distributed ltl model-checking based on accepting predecessors,
Proceedings of the 4th international workshop on parallel and distributed methods in verifiCation (pdmc 2005), 2005. [BIB]

Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, Jan Strejček:
Reachability analysis of multithreaded software with asynchronous communication,
FSTTCS 2005: Foundations of software technology and theoretical computer science: 25th international conference, hyderabad, india, december 15-18, 2005. Proceedings, 2005. [BIB] [URL]

Mojmír Křetínský, Vojtěch Řehák, Jan Strejček:
Reachability of hennessy - milner properties for weakly extended prs,
FSTTCS 2005: 25th international conference on foundations of software technology and theoretical computer science, 25th international conference, 2005. [BIB]

Antonín Kučera, Jan Strejček:
The stuttering principle revisited,
Acta informatica, 2005. [BIB]

2004

Luboš Brim, Ivana Černá, Pavel Moravec, Jiří Šimša:
Accepting predecessors are better than back edges in distributed ltl model-checking,
Formal methods in computer-aided design (fmcad), 2004. [BIB] [PDF]

Tomáš Brázdil, Antonín Kučera, Oldřich Stražovský:
Deciding probabilistic bisimilarity over infinite-state probabilistic systems,
Proceedings of 15th international conference on concurrency theory (concur 2004), 2004. [BIB]

Jiří Barnat:
Distributed Memory LTL Model Checking,
PhD thesis, 2004. [BIB]

Luboš Brim, Ivana Černá, Lukáš Hejtmánek:
Distributed negative cycle detection algorithms,
Parallel computing: Software technology, algorithms, architectures & applications, 2004. [BIB]

Mojmír Křetínský, Vojtěch Řehák, Jan Strejček:
Extended process rewrite systems: Expressiveness and reachability,
CONCUR 2004 - concurrency theory, 2004. [BIB]

David Antoš, Vojtěch Řehák, Jan Kořenek:
Hardware router’s lookup machine and its formal verification,
ICN’2004 conference proceedings, 2004. [BIB] [URL]

Jan Strejček:
Linear Temporal Logic: Expressiveness and Model Checking,
PhD thesis, 2004. [BIB] [PDF]

Gerd Behrmann, Patricia Bouyer, Kim G. Larsen, Peláne Radek:
Lower and upper bounds in zone based abstractions of timed automata,
Tools and algorithms for the construction and analysis of systems: 10th international conference, tacas 2004, held as part of the joint european conferences on theory and practice of software, etaps 2004, barcelona, spain, march 29 - april 2, 2004. Proceedings, 2004. [BIB] [URL]

Mojmír Křetínský, Vojtěch Řehák, Jan Strejček:
On extensions of process rewrite systems: Rewrite systems with weak finite-state unit,
INFINITY’2003: 5th international workshop on verification of infinite-state systems, 2004. [BIB] [URL]

Vojtěch Řehák:
Reachability for extended process rewrite systems,
MOVEP’04: 6th school on modeling and verifying parallel processes, 2004. [BIB]

Radek Pelánek:
Typical structural properties of state spaces,
Model checking software: 11th international spin workshop, barcelona, spain, april 1-3, 2004. Proceedings, 2004. [BIB] [URL]

David Šafránek:
Visual coordination diagrams,
Proceedings of the doctoral symposium of 7th international conference on the unified modeling language, 2004. [BIB] [URL]

David Šafránek:
Visual specification of systems with heterogeneous coordination models,
Proceeding of 3rd international workshop on foundations of coordination languages and software architectures, 2004. [BIB] [paper page]

2003

Ivana Černá, Radek Pelánek:
Distributed explicit fair cycle detection (set based approach),
Model checking software. 10th international spin workshop, 2003. [BIB] [PDF]

Luboš Brim, Jiří Barnat:
Distribution of explicit-state ltl model-checking,
8th international workshop on formal methods for industrial critical systems (fmics 03), 2003. [BIB]

Radek Pelánek:
LTL hierarchies and model checking,
Proceedings of the eight esslli student session, 2003. [BIB]

Jiří Barnat, Luboš Brim, Jakub Chaloupka:
Parallel Breadth-First Search LTL Model-Checking,
18th ieee international conference on automated software engineering (ase’03), 2003. [BIB]

Luboš Brim, Ivana Černá, Lukáš Hejtmánek:
Parallel algorithms for detection of negative cycles,
2003. [BIB] [PDF]

Ivana Černá, Radek Pelánek:
Relating hierarchy of temporal properties to model checking,
2003. [BIB] [PDF]

Ivana Černá, Radek Pelánek:
Relating hierarchy of temporal properties to model checking,
Mathematical foundations of computer science (mfcs), 2003. [BIB]

Gerd Behrmann, Kim G. Larsen, Radek Pelánek:
To store or not to store,
Computer aided verification (cav 2003), 2003. [BIB]

Luboš Brim, Jitka Žídková:
Using assumptions to distribute alternation free mu-calculus model checking,
2st international workshop on parallel and distributed model checking (pdmc 2003), 2003. [BIB] [URL]

David Šafránek:
Visual specification of concurrent systems,
Automated software engineering, 2003. Proceedings. 18th ieee international conference on, 2003. [BIB] [URL]

David Antoš, Jan Kořenek, Vojtěch Řehák:
Vyhledávání v ipv6 směrovači implementovaném v hradlovém poli,
EurOpen, sborník příspěvků xxiii. Konference, 2003. [BIB]

2002

Vojtěch Řehák:
$\xor$-obdd in symbolic model checking,
SOFSEM 2002: Student research forum, 2002. [BIB]

Jan Strejček:
Boundaries and efficiency of verification,
Proceedings of summer school movep 2002, 2002. [BIB]

Ivana Černá, Radek Pelánek:
Distributed explicit fair cycle detection,
2002. [BIB] [PDF]

Jiří Barnat:
How to Distribute LTL Model-checking Using Decomposition of Negative Claim Automaton,
SOFSEM 2002 student research forum, 2002. [BIB]

Tomáš Brázdil, Ivana Černá:
Local distributed model checking of regctl,
Electronic notes in theoretical computer science, 2002. [BIB]

Jiří Barnat, Tomáš Brázdil, Pavel Krčál, Vojtěch Řehák, David Šafránek:
Model Checking in IPv6 Hardware Router Design,
2002. [BIB]

Jitka Stříbrná, Ivana Černá:
Modifications of expansion trees for weak bisimulation in bpa,
Electronic notes in theoretical computer science, 2002. [BIB]

Jiří Barnat, Luboš Brim, Ivana Černá:
Property Driven Distribution of Nested DFS,
Proceeding of the 3rd international workshop on verification and computational logic (vcl’2002), 2002. [BIB]

Jiří Barnat, Luboš Brim, Ivana Černá:
Property driven distribution of Nested DFS,
Proc. Workshop on verification and computational logic, 2002. [BIB]

David Šafránek:
SGCCS: A graphical language for real-time coordination,
Proceedings of 1th international workshop on foundations of coordination languages and software architectures, 2002. [BIB] [URL] [paper page]

David Šafránek:
SGCCS: A graphical language for real-time systems,
Proceedings sofsem 2002 student research forum, 2002. [BIB] [URL] [paper page]

Antonín Kučera, Jan Strejček:
The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL,
Computer science logic: 16th international workshop, csl 2002 11th annual conference of the eacsl edinburgh, scotland, uk, september 22–25, 2002 proceedings, 2002. [BIB] [URL]

Luboš Brim, Jitka Crhová, Karen Yorav:
Using assumptions to distribute ctl model checking,
1st international workshop on parallel and distributed model checking (pdmc 2002), 2002. [BIB]

Jitka Crhová, Pavel Krčál, Jan Strejček, David Šafránek, Pavel Šimeček:
YAHODA: Verification tools database,
Proceedings of tools day, 2002. [BIB] [URL]

2001

Jiří Barnat, Luboš Brim, Jitka Stříbrná:
Distributed LTL Model-Checking in SPIN,
Proc. SPIN workshop on model checking of software, 2001. [BIB]

Luboš Brim, Ivana Černá, Pavel Krčál, Radek Pelánek:
Distributed ltl model checking based on negative cycle detection,
FST tcs 2001: Foundations of software technology and theoretical computer science, 21st conference, bangalore, india, december 13-15, 2001, proceedings, 2001. [BIB]

Luboš Brim, Ivana Černá, Pavel Krčál, Radek Pelánek:
Distributed shortest paths for directed graphs with negative edge lengths,
2001. [BIB] [PDF]

Luboš Brim, Ivana Černá, Pavel Krčál, Radek Pelánek:
How to employ reverse search in distributed single-source shortest paths,
2001. [BIB] [PDF]

Luboš Brim, Ivana Černá, Pavel Krčál, Radek Pelánek:
How to employ reverse search in distributed single-source shortest paths,
SOFSEM’01, 2001. [BIB]

Jan Strejček:
Models of Infinite-State Systems with Constraints,
Master’s Thesis, 2001. [BIB] [PDF] [URL]

Luboš Brim, Ivana Černá, Martin Nečesal:
Randomization helps in ltl model checking.,
Process algebra and probabilistic methods. Performance modelling and verification (papm-probmiv), 2001. [BIB]

Jan Strejček:
Rewrite systems with constraints,
EXPRESS’01 the 8th international workshop on expressiveness in concurrency, 2001. [BIB] [URL]

2000

Jan Strejček:
Constrained Rewrite Transition Systems,
2000. [BIB] [PDF] [URL]

Ivana Černá, Jitka Stříbrná:
Some remarks on weak bisimilarity of BPA-Processes,
2000. [BIB] [PDF]

1999

Ivana Černá, Mojmír Křetínský, Antonín Kučera:
Comparing expressibility of normed BPA and BPP processes,
Acta Informatica, 1999. [BIB]

Ivana Černá, Ondřej Klíma, Jiří Srba:
On the pattern equations,
1999. [BIB] [PDF]

Ivana Černá, Ondřej Klíma, Jiří Srba:
Pattern equations and equations with stuttering,
SOFSEM’99, 1999. [BIB]

1996

Ivana Černá, Mojmír Křetínský, Antonín Kučera:
Bisimilarity is decidable in the union of normed BPA and BPP processes,
Proceedings of the 1st international workshop on verification of infinite state systems, 1996. [BIB] [paper page]

Ivana Černá, Mojmír Křetínský, Antonín Kučera:
Comparing expressibility of normed BPA and BPP processes,
1996. [BIB] [PDF]

Ivana Černá, Mojmír Křetínský, Antonín Kučera:
On the relationship between sequential and parallel compositions in process algebras,
CSL96 - the 1996 annual conference of the european assoc.., 1996. [BIB]

Ivana Štefáneková:
Some properties of zerotesting bounded one-way multicounter machines,
1996. [BIB]

1991

Andrej Bebják, Ivana Štefáneková:
Separation of deterministic, nondeterministic and alternating complexity classes,
Theoretical Computer Science, 1991. [BIB]

1990

Ivana Štefáneková:
Some properties of zerotesting bounded one-way multicounter machines,
Proceedings of mathematical foundations of computer science, 1990. [BIB]

1989

Dana Pardubská, Ivana Štefáneková:
Nondeterministic multicounter machines and complementation,
Theoretical Computer Science, 1989. [BIB]

1988

Andrej Bebják, Ivana Štefáneková:
Nondeterminism is essential for reversal-bounded two-way multihead finite automata,
Kybernetika, 1988. [BIB]

Andrej Bebják, Ivana Štefáneková:
Relation between one-time-only braching programs and real-time branching programs,
Computers and Artificial Intelligence, 1988. [BIB]