Publications
2012
Jiri Barnat, Petr Bauch, Lubos Brim, Milan Ceska:Designing fast LTL model checking algorithms for many-core GPUs,
To appear in Journal of Parallel and Distributed Computing, 2012, -. [bibtex, pdf, url]
J. Barnat, L. Brim, A. Krejci, A. Streck, D. Safranek, M. Vejnar, T. Vejpustek:
On Parameter Synthesis by Parallel Model Checking,
To appear in IEEE/ACM Transactions on Computational Biology and Bioinformatics, volume PrePrint(99), 2012. [bibtex, pdf, url]
J. Barnat, L. Brim, P. Rockai:
On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties,
To appear in Science of Computer Programming, 2012. [bibtex, pdf, url]
B. Yordanov, J. Tumova, I. Cerna, J. Barnat, C. Belta:
Temporal Logic Control of Discrete-Time Piecewise Affine Systems,
To Appear in IEEE Transactions On Automatic Control, 2012. [bibtex, pdf]
2011
Jiri Barnat, Petr Bauch, Lubos Brim, Milan Ceska:Computing Optimal Cycle Mean in Parallel on CUDA,
Parallel and Distributed Methods in verifiCation (PDMC'11), Open Publishing Association, 2011, volume 72 of Electronic Proceedings in Theoretical Computer Science, 68-83. [bibtex, pdf, url]
J. Barnat, P. Bauch, L. Brim, M. Ceska:
Computing Strongly Connected Components in Parallel on CUDA,
Proceedings of the 25th IEEE International Parallel \& Distributed Processing Symposium (IPDPS'11), IEEE Computer Society, 2011, 541-552. [bibtex, pdf]
Plasil R.:
Counterexample explanation in DiVinE model-checker,
[bibtex, pdf, url]
J. Barnat, J. Chaloupka, J. Van De Pol:
Distributed Algorithms for SCC Decomposition,
Journal of Logic and Computation, volume 21(1), 2011, 23-44. [bibtex, pdf, url]
S. Edelkamp, D. Sulewski, J. Barnat, L. Brim, P. Simecek:
Flash memory efficient LTL model checking,
Science of Computer Programming, volume 76, 2011, 136-157. [bibtex, pdf, url]
Lubo¹ Brim, Jiøí Barnat:
Platform Dependent Verification: On Engineering Verification Tools for 21st Century,
Parallel and Distributed Methods in verifiCation (PDMC'11), Open Publishing Association, 2011, volume 72 of Electronic Proceedings in Theoretical Computer Science, 1-12. [bibtex, pdf]
Brim:
Reachability in Biochemical Dynamical Systems by Quantitative Discrete Approximation,
ArXiv e-prints, 2011, month = jul, adsurl = http://adsabs.harvard.edu/abs/2011arXiv1107.5924B. [bibtex, pdf]
J. Barnat, I. Cerna, J. Tumova:
Timed Automata Approach to Verification of Systems with Degradation,
Proceedings of Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2011), Springer, 2011, volume 7119 of LNCS, 86-95. [bibtex, pdf]
2010
J. Tumova, B. Yordanov, C. Belta, I. Cerna, J. Barnat:A Symbolic Approach to Controlling Piecewise Affine Systems,
41th IEEE Conference on Decision and Control (CDC'10), IEEE, 2010, 4230-4235. [bibtex, pdf]
J. Barnat, L. Brim, M. Ceska, P. Rockai:
DiVinE: Parallel Distributed Model Checker (Tool paper),
Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology (HiBi/PDMC 2010), IEEE, 2010, 4-7. [bibtex, pdf]
J. Barnat, P. Bauch, L. Brim, M. Ceska:
Employing Multiple CUDA Devices to Accelerate LTL Model Checking,
16th International Conference on Parallel and Distributed Systems (ICPADS 2010), IEEE Computer Society, 2010, 259-266. [bibtex, pdf]
B. Yordanov, J. Tumova, C. Belta, I. Cerna, J. Barnat:
Formal Analysis of Piecewise Affine Systems through Formula-Guided Refinement,
41th IEEE Conference on Decision and Control (CDC'10), IEEE, 2010, 5899-5904. [bibtex, pdf]
J. Barnat, L. Brim, D. Safranek:
High-Performance Analysis of Biological Systems Dynamics with the DiVinE Model Checker,
Briefings in Bioinformatics, volume 11(3), 2010, 301-312. [bibtex, pdf, url]
J. Barnat, L. Brim, P. Rockai:
Parallel Partial Order Reduction with Topological Sort Proviso,
Software Engineering and Formal Methods (SEFM 2010), IEEE Computer Society Press, 2010, 222-231. [bibtex, pdf]
J. Barnat, L. Brim, D. Safranek, M. Vejnar:
Parameter Scanning by Parallel Model Checking with Applications in Systems Biology,
Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology (HiBi/PDMC 2010), IEEE, 2010., 95-104. [bibtex, pdf]
J. Barnat, L. Brim, P. Rockai:
Scalable shared memory LTL model checking,
International Journal on Software Tools for Technology Transfer (STTT), volume 12(2), 2010, 139-153. [bibtex, pdf, url]
2009
J. Barnat, L. Brim, P. Rockai:A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties,
Formal Methods and Software Engineering (ICFEM 2009), Springer, 2009, volume 5885 of LNCS, 407-425. [bibtex, pdf]
J. Barnat, L. Brim, I. Cerna, S. Drazan, J. Fabrikova, J. Lanik, D. Safranek, Hongwu Ma:
BioDiVinE: A Framework for Parallel Analysis of Biological Models,
Electronic Proceedings in Theoretical Computer Science (COMPMOD 2009), volume 6, 2009, 31-45. [bibtex, pdf, url]
J. Barnat, L. Brim, I. Cerna, S. Drazan, J. Fabrikova, J. Lanik, D. Safranek:
BioDiVinE: A Tool for Parallel Analysis of Multi-Affine ODE Models,
Proceedings of The 7th Conference on Computational Methods in Systems Biology (CMSB'09), Universita di Pisa, 2009, volume TR-09-09 of Technical Report, 1--5. [bibtex, pdf]
J. Barnat, L. Brim, P. Simecek:
Cluster-Based I/O Efficient LTL Model Checking,
24th IEEE/ACM International Conference on Automated Software Engineering (ASE 2009), IEEE Computer Society, 2009, 635-639. [bibtex, pdf]
J. Barnat, L. Brim, I. Cerna, S. Drazan, J. Fabrikova, D. Safranek:
Computational Analysis of Large-Scale Multi-Affine ODE Models,
2009 International Workshop on High Performance Computational Systems Biology (HiBi 2009), IEEE Computer Society Press, 2009, 81-90. [bibtex, pdf]
J. Barnat, L. Brim, M. Ceska, T. Lamr:
CUDA accelerated LTL Model Checking,
15th International Conference on Parallel and Distributed Systems (ICPADS 2009), IEEE Computer Society, 2009, 34-41. [bibtex, pdf]
Jiri Barnat, Lubos Brim, Petr Rockai:
DiVinE 2.0: High-Performance Model Checking,
2009 International Workshop on High Performance Computational Systems Biology (HiBi 2009), IEEE Computer Society Press, 2009, 31-32. [bibtex, pdf]
J. Barnat, L. Brim, M. Ceska:
DiVinE-CUDA: A Tool for GPU Accelerated LTL Model Checking,
Electronic Proceedings in Theoretical Computer Science (PDMC 2009), volume 14, 2009, 107-111. [bibtex, pdf, url]
K. Verstoep, H. Bal, J. Barnat, L. Brim:
Efficient Large-Scale Model Checking,
23rd IEEE International Parallel & Distributed Processing Symposium (IPDPS 2009), IEEE, 2009. [bibtex, pdf]
J. Barnat, L. Brim, I. Cerna, S. Drazan, J. Fabrikova, D. Safranek:
On algorithmic analysis of transcriptional regulation by LTL model checking,
Theor. Comput. Sci., volume 410(33-34), 2009, 3128-3148. [bibtex, pdf, url]
Nikola Benes, Lubos Brim, Ivana Cerna, Jiri Sochor, Pavlina Varekova, Barbora Zimmerova:
Partial Order Reduction for State/Event LTL,
Proceedings of the International Conference on Integrated Formal Methods (IFM'09), Springer-Verlag, 2009, volume 5423 of LNCS, 307--321. [bibtex, pdf]
J. Barnat, I. Cerna, J. Tumova:
Quantitative Model Checking of Systems with Degradation,
Proceeding of the Sixth International Conference on Quantitative Evaluation of Systems (QEST 2009), IEEE, 2009, 21-30. [bibtex, pdf]
2008
Nikola Benes, Ivana Cerna, Jiri Sochor, Pavlina Varekova, Barbora Zimmerova:A Case Study in Parallel Verification of Component-Based Systems,
Electr. Notes Theor. Comput. Sci., volume 220(2), 2008, 67-83. [bibtex, pdf, url]
P. Varekova, I. Varekova, I. Cerna:
Automated Computing of the Maximal Number of Handled Clients for Client-Server Systems,
Proceedings of FACS'08, 2008, 41--55. [bibtex, pdf]
J. Barnat, L. Brim, S. Edelkamp, D. Sulewski, P. Simecek:
Can Flash Memory Help in Model Checking,
Formal Methods for Industrial Critical Systems (FMICS 2008), Springer-Verlag, 2008, volume 5596 of LNCS, 150--165. [bibtex, pdf]
J. Barnat, L. Brim, P. Rockai:
DiVinE Multi-Core -- A Parallel LTL Model-Checker,
Automated Technology for Verification and Analysis (ATVA 2008), Springer, 2008, volume 5311 of LNCS, 234-239. [bibtex, pdf]
R. Pelanek:
Fighting State Space Explosion: Review and Evaluation,
13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008), ERCIM, 2008, 47--62. [bibtex, pdf]
Pavlina Varekova, Barbora Zimmerova, Pavel Moravec, Ivana Cerna:
Formal Verification of Systems with an Unlimited Number of Components,
IET Software journal, volume 2(6), December 2008, 532--546. [bibtex, pdf]
J. Barnat, J. Chaloupka, J. van de Pol:
Improved Distributed Algorithms for SCC Decomposition,
ENTCS, volume 198(1), 2008, 63--77. [bibtex, pdf]
J. Barnat, L. Brim, I. Cerna, M. Ceska, J. Tumova:
Local Quantitative LTL Model Checking,
Formal Methods for Industrial Critical Systems (FMICS 2008), Springer-Verlag, 2008, volume 5596 of LNCS, 53--68. [bibtex, pdf]
P. Varekova, I. Cerna:
Model Checking of Control-User Component-Based Parametrised Systems,
CBSE'08, Springer, 2008, volume 5282 of Lecture Notes in Computer Science, 146-162. [bibtex, pdf]
J. Barnat, L. Brim, I. Cerna, S. Drazan, D. Safranek:
Parallel Model Checking Large-Scale Genetic Regulatory Networks with DiVinE,
ENTCS, volume 194(3), 2008, 35--50. [bibtex, pdf]
J. Barnat, L. Brim, I. Cerna, M. Ceska, J. Tumova:
ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems,
QEST '08: Proceedings of the 2008 Fifth International Conference on Quantitative Evaluation of Systems, IEEE Computer Society, 2008, 77--78. [bibtex, pdf]
J. Barnat, L. Brim, P. Simecek, M. Weber:
Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking,
Tools and Algorithms for the Construction and Analysis of Systems (TACAS)., Springer, 2008, volume 4963 of LNCS, 48-62. [bibtex, pdf]
Stefan Edelkamp, Peter Sanders, Pavel Simecek:
Semi-external LTL Model Checking,
Computer Aided Verification, Springer, 2008, volume 5123 of LNCS, 530-542. [bibtex, pdf]
J. Barnat, P. Rockai:
Shared Hash Tables in Parallel Model Checking,
ENTCS, volume 198(1), 2008, 79--91. [bibtex, pdf]
L. Brim, J.Barnat:
Squeeze All the Power Out of Your Hardware to Verify Your Software!,
ISOLA 2008, Springer Verlag, 2008, volume 17 of CCIS, 604-618. [bibtex, pdf]
Nikola Benes, Lubos Brim, Ivana Cerna, Jiri Sochor, Pavlina Varekova, Barbora Zimmerova:
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, 221--225. [bibtex, pdf]
Barbora Zimmerova, Pavlina Varekova, Nikola Benes, Ivana Cerna, Lubos Brim, Jiri Sochor:
The Common Component Modeling Example: Comparing Software Component Models,
[bibtex, pdf]
2007
R. Pelanek:BEEM: Benchmarks for Explicit Model Checkers,
Model Checking Software (SPIN 2007), Springer, 2007, volume 4595 of LNCS, 263--267. [bibtex, pdf]
Pavlina Varekova, Barbora Zimmerova:
Challenge Problem: Subject-Observer Specification with Component-Interaction Automata,
Proceedings of the ESEC/FSE Conference on Specification and Verification of Component-Based Systems (SAVCBS'07), ACM Press, 2007, 75--81. [bibtex, pdf, url]
Ivana Cerna, Pavlina Varekova, Barbora Zimmerova:
Component Substitutability via Equivalencies of Component-Interaction Automata,
Electronic Notes in Theoretical Computer Science, volume 182, June 2007, 39--55. [bibtex, pdf, url]
L. Brim:
Distributed Verification: Exploring the Power of Raw Computing Power,
Formal Methods, Applications and Technology, Springer, 2007, volume 4346 of LNCS, 244-260. [bibtex, pdf]
L. Brim:
Distributed Verification: Exploring the Power of Raw Computing Power,
Formal Methods: Applications and Technology, Springer, 2007, volume 4346 of LNCS, 23-34. [bibtex, pdf]
Pavlina Varekova, Pavel Moravec, Ivana Cerna, Barbora Zimmerova:
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), ACM Press, 2007, 3--13. [bibtex, pdf, url]
J. Barnat, L. Brim, P. Simecek:
I/O Efficient Accepting Cycle Detection,
Computer Aided Verification, Springer, 2007, volume 4590 of LNCS, 281--293. [bibtex, pdf]
R. Pelanek:
Model Classifications and Automated Verification,
12th Internacional ERCIM Workshop on Formal Methods for Industrial Critical Systems (FMICS'07), Universit\at Konstanz, 2007, 149--162. [bibtex, pdf]
Lubos Brim, Mojmir Kretinsky:
Model-Checking Large Finite-State Systems and Beyond,
SOFSEM 2007: Theory and Practice of Computer Science, Springer, 2007, volume 4362 of LNCS, 9-28. [bibtex, pdf]
Lubos Brim, Ivana Cerna, Pavel Moravec, Jiri Simsa:
On Combining Partial Order Reduction with Fairness Assumptions,
FMICS/PDMC, 2007, volume 4346 of Lecture Notes in Computer Science, 84 -- 99. [bibtex, pdf]
Jiri Barnat, Lubos Brim, Martin Leucker:
Parallel Model Checking and the FMICS-jETI Platform,
The Twelfth IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2007), IEEE Computer Society Press, 2007. [bibtex, pdf]
J. Barnat, L. Brim, I. Cerna, S. Drazan, D.Safranek:
Parallel Model-Checking Genetic Regulatory Networks,
Towards Systems Biology, Verimag, 2007. [bibtex, pdf]
J. Barnat, L. Brim, I. Cerna, M. Ceska, J. Tumova:
ProbDiVinE: A Parallel Qualitative LTL Model Checker,
Fourth International Conference on the Quantitative Evaluation of Systems (QEST'07), IEEE Computer Society, 2007, 215-216. [bibtex, pdf]
J. Barnat, L. Brim, P. Rockai:
Scalable Multi-core LTL Model-Checking,
Model Checking Software, Springer, 2007, volume 4595 of LNCS, 187--203. [bibtex, pdf]
L. Brim, J. Barnat:
Tutorial: Parallel Model Checking,
Model Checking Software, Springer, 2007, volume 4595 of LNCS, 2--3. [bibtex, pdf]
2006
Lubos Brim, Ivana Cerna, Pavlina Varekova, Barbora Zimmerova:Component-interaction automata as a verification-oriented component-based system specification,
ACM SIGSOFT Software Engineering Notes, volume 31(2), 2006. [bibtex, pdf]
Jiri Barnat, Ivana Cerna:
Distributed Breadth-First Search LTL Model Checking,
Special Issue on Parallel and Distributed Databases of Formal Methods in System Design, volume 29(2), September 2006, 117-134(18). [bibtex, pdf]
J. Barnat, L. Brim, I. Cerna, P. Moravec, P. Rockai, P. Simecek:
DiVinE -- A Tool for Distributed Verification (Tool Paper),
Computer Aided Verification, Springer Berlin / Heidelberg, 2006, volume 4144/2006 of LNCS, 278-281. [bibtex, pdf]
Lubos Brim, Ivana Cerna, Pavel Moravec, Jiri Simsa:
How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors,
Electr. Notes Theor. Comput. Sci., volume 135(2), 2006, 3-18. [bibtex, pdf]
Tomas Brazdil, Ivana Cerna:
Model Checking of RegCTL,
Computers and Artificial Intelligence, volume 25(1), 2006. [bibtex, pdf]
Jiri Simsa:
Monitoring of Systems Behaviour,
Master's Thesis, Faculty of Informatics, Masaryk University, Brno, 2006. [bibtex, pdf]
Laura Bozzelli, Mojmir Kretinsky, Vojtech Rehak, Jan Strejcek:
On Decidability of LTL model Checking for Process Rewrite Systems,
FSTTCS 2006, Springer-Verlag, 2006, volume 4337 of Lecture Notes in Computer Science, 248--259. [bibtex, pdf]
Ahmed Bouajjani, Jan Strejcek, Tayssir Touili:
On Symbolic Verification of Weakly Extended PAD,
EXPRESS 2006, Elsevier Science Publishers, 2006, Electronic Notes in Theoretical Computer Science. [bibtex, pdf]
Jiri Barnat, Pavel Moravec:
Parallel Algorithms for Finding SCCs in Implicitly Given Graphs,
Formal Methods: Applications and Technology, Springer, 2006, volume 4346 of LNCS, 316--330. [bibtex, pdf]
2005
J. Barnat, L. Brim, I. Cerna:Cluster-Based LTL Model Checking of Large Systems,
Formal Methods for Components and Objects, 2005, LNCS, 259-279. [bibtex, pdf]
Radek Pelanek, Jan Strejcek:
Deeper Connections between LTL and Alternating Automata,
CIAA 2005, Springer-Verlag, 2005, Lecture Notes in Computer Science. [bibtex, pdf]
Lubos Brim, Ivana Cerna, Pavel Moravec, Jiri Simsa:
Distributed Partial Order Reduction of State Spaces,
Electr. Notes Theor. Comput. Sci., volume 128(3), 2005, 63-74. [bibtex, pdf]
J. Barnat, L. Brim, I. Cerna, P. Simecek:
DiVinE -- The Distributed Verification Environment,
Proceedings of 4th International Workshop on Parallel and Distributed Methods in verifiCation, 2005, 89--94. [bibtex, pdf]
J. Barnat, V. Forejt, M. Leucker, M. Weber:
DivSPIN -- A SPIN compatible distributed model checker,
Proceedings of 4th International Workshop on Parallel and Distributed Methods in verifiCation, 2005, 95--100. [bibtex, pdf]
J. Barnat, L. Brim, J. Chaloupka:
From Distributed Memory Cycle Detection to Parallel LTL Model Checking,
Electronic Notes in Theoretical Computer Science, volume 133(1), 2005, 21--39. [bibtex, pdf]
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, 2005, 186-192. [bibtex, pdf]
L. Brim, I. Cerna, P. Moravec, J. Simsa:
How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors,
4rd International Workshop on Parallel and Distributed Methods in verifiCation, 2005. [bibtex, pdf]
Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, Jan Strejcek:
Reachability Analysis of Multithreaded Software with Asynchronous Communication,
FSTTCS 2005, Springer-Verlag, 2005, volume 3821 of Lecture Notes in Computer Science, 348--359. [bibtex, pdf]
M. Kretinsky, V. Rehak, J. Strejcek:
Reachability of Hennessy--Milner Properties for Weakly Extended PRS,
Proceedings of 25th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'05), 2005, Lecture Notes in Computer Science. [bibtex, pdf]
Antonin Kucera, Jan Strejcek:
The Stuttering Principle Revisited,
Acta Informatica, volume 41(7--8), 2005, 415--434. [bibtex, pdf]
2004
L. Brim, I. Cerna, P. Moravec , J. Simsa:Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking,
5th International Conference on Formal Methods in Computer-Aided Design (FMCAD'04), Springer-Verlag, 2004, volume 3312 of LNCS, 352-366. [bibtex, pdf]
T. Brazdil, A. Kucera, O. Strazovsky:
Deciding Probabilistic Bisimilarity over Infinite-State Probabilistic Systems,
CONCUR 2004 -- Concurrency Theory: 15th International Conference, Springer-Verlag, 2004, series = Lecture Notes in Computer Science, volume 3170 of , 193--208. [bibtex, pdf]
Jiri Barnat:
Distributed Memory LTL Model Checking,
Ph.D. Thesis, Masaryk University Brno, Faculty of Informatics, 2004. [bibtex, pdf]
Lubos Brim, Ivana Cerna, Lukas Hejtmanek:
Distributed Negative Cycle Detection Algorithms,
Parallel Computing: Software Technology, Algorithms, and Applications (PARCO'03), Elsevier, 2004, volume 13 of Advances in Parallel Computing, 297--304. [bibtex, pdf]
M. Kretinsky, V. Rehak, J. Strejcek:
Extended Process Rewrite Systems: Expressiveness and Reachability,
CONCUR 2004 -- Concurrency Theory: 15th International Conference, Springer-Verlag, 2004, series = Lecture Notes in Computer Science, volume 3170 of , 355--370. [bibtex, pdf]
D. Antos, V. Rehak, J. Korenek:
Hardware Router's Lookup Machine and its Formal Verification,
ICN'2004 Conference Proceedings. Gosier, Guadeloupe, French Caribbean, 2004, 1002-1007. [bibtex, pdf]
Jan Strejcek:
Linear Temporal Logic: Expressiveness and Model Checking,
Ph.D. Thesis, Faculty of Informatics, Masaryk University in Brno, 2004. [bibtex, pdf]
G. Behrmann, P. Bouyer, K. G. Larsen, R. Pelanek:
Lower and Upper Bounds in Zone Based Abstractions of Timed Automata,
Proc. of Tools and Algorithms for Construction and Analysis of Systems (TACAS 2004), 2004, volume 2988 of LNCS, 312-326. [bibtex, pdf]
V. Rehak:
Reachability for Extended Process Rewrite Systems,
MOVEP'04: 6th school on MOdeling and VErifying parallel Processes, 2004, publisher = Universite Libre de Bruxelles, 77--82. [bibtex, pdf]
R. Pelanek:
Typical Structural Properties of State Spaces,
Proc. of SPIN Workshop, 2004, volume 2989 of LNCS, 5-22. [bibtex, pdf]
David Safranek:
Visual Coordination Diagrams,
Proceedings of UML'04 Doctoral Symposium, Alanen M., Cabot J., Goulao M., Saez J. and Simmonds D. (editors), 2004. [bibtex, pdf]
David Safranek:
Visual Specification of Systems with Heterogeneous Coordination Models,
Proceedings of FOCLASA'04, Elsevier Science, 2004, ENTCS. [bibtex, pdf]
2003
I. Cerna, R. Pelanek:Distributed Explicit Fair Cycle Detection,
Proc. SPIN workshop, Springer, 2003, volume 2648 of LNCS, 49-74. [bibtex, pdf]
L. Brim, J. Barnat:
Distribution of Explicit-State LTL Model-Checking,
8th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 03), Elsevier, 2003, volume 80 of Electronic Notes in Theoretical Computer Science. [bibtex, pdf]
R. Pelanek:
LTL Hierarchies and Model Checking,
ESSLLI Student Session, 2003. [bibtex, pdf]
M. Kretinsky, V. Rehak, J. Strejcek:
On Extensions of Process Rewrite Systems: Rewrite Systems with Weak Finite-State Unit,
INFINITY'2003: 5th International Workshop on Verification of Infinite-State Systems, Elsevier Science Publishers, 2004, volume 98 of Electronic Notes in Theoretical Computer Science, 75--88. [bibtex, pdf]
J. Barnat, L. Brim, J. Chaloupka:
Parallel Breadth-First Search LTL Model-Checking,
18th IEEE International Conference on Automated Software Engineering (ASE'03), IEEE Computer Society, 2003, 106--115. [bibtex, pdf]
I. Cerna, R. Pelanek:
Relating Hierarchy of Temporal Properties to Model Checking,
Mathematical Foundations of Computer Science (MFCS), Springer, 2003, volume 2747 of LNCS, 318-327. [bibtex, pdf]
G. Behrmann, K.G. Larsen, R. Pelanek:
To Store or Not To Store,
Proc. Computer Aided Verification (CAV'03), 2003, volume 2725 of LNCS, 433-445. [bibtex, pdf]
Brim, L., Zidkova:
Using Assumptions to Distribute Alternation Free mu-calculus Model Checking,
2nd International Workshop on Parallel and Distributed Model Checking (PDMC 2003), Elsevier, 2003, volume = 89, series = ENTCS, 19-34. [bibtex, pdf]
David Safranek:
Visual Specification of Concurrent Systems,
Proceedings of 18th IEEE International Conference on Automated Software Engineering, IEEE Computer Society, 2003. [bibtex, pdf]
D. Antos, J. Korenek, V. Rehak:
Vyhledavani v IPv6 smerovaci implementovanem v hradlovem poli,
EurOpen, Sbornik prispevku XXIII. konference. Straznice: EurOpen, 2003, 91--102. [bibtex, pdf]
2002
Vojtech Rehak:$\xor$-OBDD in Symbolic Model Checking,
Proceedings of SOFSEM'02 Student Research Forum, 2002, 41--46. [bibtex, pdf]
J. Strejcek:
Boundaries and Efficiency of Verification,
Proceedings of summer school on MOdelling and VErification of Parallel processes (MOVEP~'02), IRCCyN, Ecole Centrale de Nantes, 2002, 403--408. [bibtex, pdf]
J. Barnat:
How to Distribute LTL Model-checking Using Decomposition of Negative Claim Automaton,
SOFSEM 2002 Student Research Forum, 2002, 9--14. [bibtex, pdf]
Tomas Brazdil, Ivana Cerna:
Local Distributed Model Checking of RegCTL,
Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers, 2002, volume 68 of . [bibtex, pdf]
Jitka Stribrna, Ivana Cerna:
Modifications of Expansion Trees for Weak Bisimulation in BPA,
Electr. Notes Theor. Comput. Sci., volume 68(6), 2002. [bibtex, pdf]
J. Barnat, L. Brim, I. Cerna:
Property driven distribution of Nested DFS,
Proc. Workshop on Verification and Computational Logic, 2002, DSSE Technical Report, 1 - 10. [bibtex, pdf]
David Safranek:
SGCCS: A Graphical Language for Real-Time Coordination,
Proceedings of FOCLASA'02, Elsevier Science, 2002, volume 68 of ENTCS. [bibtex, pdf]
David Safranek:
SGCCS: A Graphical Language for Real-Time Systems,
Proceedings of SOFSEM'02 Student Research Forum, 2002. [bibtex, pdf]
Antonin Kucera, Jan Strejcek:
The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL,
CSL~'02: 11th Annual Conference of the European Association for Computer Science Logic, Springer-Verlag, 2002, volume 2471 of Lecture Notes in Computer Science, 276--291. [bibtex, pdf]
Lubos Brim, Jitka Crhova, Karen Yorav:
Using Assumptions to Distribute CTL Model Checking,
Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers, 2002, volume 68 of . [bibtex, pdf]
J. Crhova, P. Krcal, J. Strejcek, D. Safranek, P. Simecek:
YAHODA: Verification Tools Database,
Proc. of TOOLSDAY affiliated to CONCUR 2002, FI MU report series, 2002. [bibtex, pdf]
2001
L. Brim, I. Cerna, P. Krcal , R. Pelanek:Distributed LTL Model Checking Based on Negative Cycle Detection,
Proc. Foundations of Software Technology and Theoretical Computer Science 2001, Springer, 2001, volume 2245 of Lecture Notes in Computer Science, 96 -- 107. [bibtex, pdf]
J. Barnat, L. Brim, J. Stribrna:
Distributed LTL Model-Checking in SPIN,
Proc. SPIN Workshop on Model Checking of Software, Springer, 2001, volume 2057 of LNCS, 200 - 216. [bibtex, pdf]
L. Brim, I. Cerna, P. Krcal, R. Pelanek:
How to Employ Reverse Search in Distributed Single-Source Shortest Paths,
Proc. of SOFSEM'01, Springer, 2001, volume 2234 of LNCS, 191--200. [bibtex, pdf]
J. Strejcek:
Models of infinite-state systems with constraints,
Master's Thesis, Faculty of Informatics, Masaryk University in Brno, 2001. [bibtex, pdf]
Lubos Brim, Ivana Cerna, Martin Necesal:
Randomization Helps in LTL Model Checking,
Proc. of PAPM-PROBMIV 2001, Springer, 2001, volume 2165 of LNCS, 105-119. [bibtex, pdf, url]
J. Strejcek:
Rewrite Systems with Constraints,
EXPRESS'01: 8th International Workshop on Expressiveness in Concurrency, 2002, series = Electronic Notes in Theoretical Computer Science, volume 52, publisher = Elsevier Science Publishers of . [bibtex, pdf]
2000
J. Strejcek:Constrained Rewrite Transition Systems,
Master's Thesis, Faculty of Science, Masaryk University, 2000. [bibtex, pdf]
1999
Ivana Cerna, Mojmir Kretinsky, Antonin Kucera:Comparing Expressibility of Normed BPA and Normed BPP Processes,
Acta Inf., volume 36(3), 1999, 233-256. [bibtex, pdf]
Ivana Cerna, Ondrej Klima, Jiri Srba:
Pattern Equations and Equations with Stuttering,
Proc. of SOFSEM'99, Springer, 1999, volume 1725 of LNCS, 369 -- 378. [bibtex, pdf]
1990
Ivana Cerna:Mathematical Foundations of Computer Science (MFCS'90),
MFCS, Springer, 1990, volume 452 of Lecture Notes in Computer Science, 195-201. [bibtex, pdf]