Jiri Barnat and Petr Bauch and Lubos Brim and Milan Ceska:
Designing fast LTL model checking algorithms for many-core GPUs [bibtex, pdf, url] To appear in Journal of Parallel and Distributed Computing, 2012, -.
J. Barnat and L. Brim and A. Krejci and A. Streck and D. Safranek and M. Vejnar and T. Vejpustek:
On Parameter Synthesis by Parallel Model Checking [bibtex, pdf, url] To appear in IEEE/ACM Transactions on Computational Biology and Bioinformatics, volume PrePrint(99), 2012.
J. Barnat and L. Brim and P. Rockai:
On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties [bibtex, pdf, url] To appear in Science of Computer Programming, 2012.
B. Yordanov and J. Tumova and I. Cerna and J. Barnat and C. Belta:
Temporal Logic Control of Discrete-Time Piecewise Affine Systems [bibtex, ] To Appear in IEEE Transactions On Automatic Control, 2012.
J. Barnat and L. Brim and P. Ročkai:
Towards LTL Model Checking of Unmodified Thread-Based C \& C++ Programs [bibtex, pdf] To appear in NASA Formal Methods Symposium, Springer, 2012, LNCS.
2011
Jiri Barnat and Petr Bauch and Lubos Brim and Milan Ceska:
Computing Optimal Cycle Mean in Parallel on CUDA [bibtex, pdf, url] Parallel and Distributed Methods in verifiCation (PDMC'11), Open Publishing Association, 2011, volume 72 of Electronic Proceedings in Theoretical Computer Science, 68-83.
J. Barnat and P. Bauch and L. Brim and M. Ceska:
Computing Strongly Connected Components in Parallel on CUDA [bibtex, pdf] Proceedings of the 25th IEEE International Parallel \& Distributed Processing Symposium (IPDPS'11), IEEE Computer Society, 2011, 541-552.
J. Barnat and J. Chaloupka and J. Van De Pol:
Distributed Algorithms for SCC Decomposition [bibtex, pdf, url] Journal of Logic and Computation, volume 21(1), 2011, 23-44.
S. Edelkamp and D. Sulewski and J. Barnat and L. Brim and P. Simecek:
Flash memory efficient LTL model checking [bibtex, url] Science of Computer Programming, volume 76, 2011, 136-157.
Luboš Brim and Jiří Barnat:
Platform Dependent Verification: On Engineering Verification Tools for 21st Century [bibtex, pdf] Parallel and Distributed Methods in verifiCation (PDMC'11), Open Publishing Association, 2011, volume 72 of Electronic Proceedings in Theoretical Computer Science, 1-12.
J. Barnat and I. Cerna and J. Tumova:
Timed Automata Approach to Verification of Systems with Degradation [bibtex, pdf] Proceedings of Annual Doctoral Workshop on Mathematical and
Engineering Methods in Computer Science (MEMICS 2011), Springer, 2011, volume 7119 of LNCS, 86-95.
2010
J. Tumova and B. Yordanov and C. Belta and
I. Cerna and J. Barnat:
A Symbolic Approach to Controlling Piecewise Affine Systems [bibtex, pdf] 41th IEEE Conference on Decision and Control (CDC'10), IEEE, 2010, 4230-4235.
J. Barnat and L. Brim and M. Ceska and P. Rockai:
DiVinE: Parallel Distributed Model Checker (Tool paper) [bibtex, pdf] Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology (HiBi/PDMC 2010), IEEE, 2010, 4-7.
J. Barnat and P. Bauch and L. Brim and M. Ceska:
Employing Multiple CUDA Devices to Accelerate LTL Model Checking [bibtex, pdf] 16th International Conference on Parallel and Distributed Systems (ICPADS 2010), IEEE Computer Society, 2010, 259-266.
B. Yordanov and J. Tumova and C. Belta and
I. Cerna and J. Barnat:
Formal Analysis of Piecewise Affine Systems through Formula-Guided Refinement [bibtex, pdf] 41th IEEE Conference on Decision and Control (CDC'10), IEEE, 2010, 5899-5904.
J. Barnat and L. Brim and D. Safranek:
High-Performance Analysis of Biological Systems Dynamics with the DiVinE Model Checker [bibtex, pdf, url] Briefings in Bioinformatics, volume 11(3), 2010, 301-312.
J. Barnat and L. Brim and P. Rockai:
Parallel Partial Order Reduction with Topological Sort Proviso [bibtex, pdf] Software Engineering and Formal Methods (SEFM 2010), IEEE Computer Society Press, 2010, 222-231.
J. Barnat and L. Brim and D. Safranek and M. Vejnar:
Parameter Scanning by Parallel Model Checking with
Applications in Systems Biology [bibtex, pdf] Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology (HiBi/PDMC 2010), IEEE, 2010., 95-104.
J. Barnat and L. Brim and P. Rockai:
Scalable shared memory LTL model checking [bibtex, pdf, url] International Journal on Software Tools for Technology Transfer (STTT), volume 12(2), 2010, 139-153.
2009
J. Barnat and L. Brim and P. Rockai:
A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties [bibtex, pdf] Formal Methods and Software Engineering (ICFEM 2009), Springer, 2009, volume 5885 of LNCS, 407-425.
J. Barnat and L. Brim and I. Cerna and S. Drazan and J. Fabrikova and J. Lanik and D. Safranek and Hongwu Ma:
BioDiVinE: A Framework for Parallel Analysis of Biological Models [bibtex, pdf, url] Electronic Proceedings in Theoretical Computer Science (COMPMOD 2009), volume 6, 2009, 31-45.
J. Barnat and L. Brim and I. Cerna and S. Drazan and J. Fabrikova and J. Lanik and D. Safranek:
BioDiVinE: A Tool for Parallel Analysis of Multi-Affine ODE Models [bibtex, pdf] 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.
J. Barnat and L. Brim and P. Simecek:
Cluster-Based I/O Efficient LTL Model Checking [bibtex, pdf] 24th IEEE/ACM International Conference on Automated Software Engineering (ASE 2009), IEEE Computer Society, 2009, 635-639.
J. Barnat and L. Brim and I. Cerna and S. Drazan and J. Fabrikova and D. Safranek:
Computational Analysis of Large-Scale Multi-Affine ODE Models [bibtex, pdf] 2009 International Workshop on High Performance Computational Systems Biology (HiBi 2009), IEEE Computer Society Press, 2009, 81-90.
J. Barnat and L. Brim and M. Ceska and T. Lamr:
CUDA accelerated LTL Model Checking [bibtex, pdf] 15th International Conference on Parallel and Distributed Systems (ICPADS 2009), IEEE Computer Society, 2009, 34-41.
Jiri Barnat and Lubos Brim and Petr Rockai:
DiVinE 2.0: High-Performance Model Checking [bibtex, pdf] 2009 International Workshop on High Performance Computational Systems Biology (HiBi 2009), IEEE Computer Society Press, 2009, 31-32.
J. Barnat and L. Brim and M. Ceska:
DiVinE-CUDA: A Tool for GPU Accelerated LTL Model Checking [bibtex, pdf, url] Electronic Proceedings in Theoretical Computer Science (PDMC 2009), volume 14, 2009, 107-111.
K. Verstoep and H. Bal and J. Barnat and L. Brim:
Efficient Large-Scale Model Checking [bibtex, pdf] 23rd IEEE International Parallel & Distributed Processing Symposium (IPDPS 2009), IEEE, 2009.
J. Barnat and L. Brim and I. Cerna and S. Drazan and J. Fabrikova and D. Safranek:
On algorithmic analysis of transcriptional regulation by LTL model checking [bibtex, pdf, url] Theor. Comput. Sci., volume 410(33-34), 2009, 3128-3148.
J. Barnat and I. Cerna and J. Tumova:
Quantitative Model Checking of Systems with Degradation [bibtex, pdf] Proceeding of the Sixth International Conference
on Quantitative Evaluation of Systems (QEST 2009), IEEE, 2009, 21-30.
2008
J. Barnat and L. Brim and S. Edelkamp and D. Sulewski and P. Simecek:
Can Flash Memory Help in Model Checking [bibtex, pdf] Formal Methods for Industrial Critical Systems (FMICS 2008), Springer-Verlag, 2008, volume 5596 of LNCS, 150--165.
J. Barnat and L. Brim and P. Rockai:
DiVinE Multi-Core -- A Parallel LTL Model-Checker [bibtex, pdf] Automated Technology for Verification and Analysis (ATVA 2008), Springer, 2008, volume 5311 of LNCS, 234-239.
J. Barnat and J. Chaloupka and J. van de Pol:
Improved Distributed Algorithms for SCC Decomposition [bibtex, pdf] ENTCS, volume 198(1), 2008, 63--77.
J. Barnat and L. Brim and I. Cerna and M. Ceska and J. Tumova:
Local Quantitative LTL Model Checking [bibtex, pdf] Formal Methods for Industrial Critical Systems (FMICS 2008), Springer-Verlag, 2008, volume 5596 of LNCS, 53--68.
J. Barnat and L. Brim and I. Cerna and S. Drazan and D. Safranek:
Parallel Model Checking Large-Scale Genetic Regulatory Networks with DiVinE [bibtex, pdf] ENTCS, volume 194(3), 2008, 35--50.
J. Barnat and L. Brim and I. Cerna and M. Ceska and J. Tumova:
ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems [bibtex, pdf] QEST '08: Proceedings of the 2008 Fifth International Conference on Quantitative Evaluation of Systems, IEEE Computer Society, 2008, 77--78.
J. Barnat and L. Brim and P. Simecek and M. Weber:
Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking [bibtex, pdf] Tools and Algorithms for the Construction and Analysis of Systems (TACAS)., Springer, 2008, volume 4963 of LNCS, 48-62.
J. Barnat and P. Rockai:
Shared Hash Tables in Parallel Model Checking [bibtex, pdf] ENTCS, volume 198(1), 2008, 79--91.
L. Brim and J.Barnat:
Squeeze All the Power Out of Your Hardware to Verify Your Software! [bibtex, pdf] ISOLA 2008, Springer Verlag, 2008, volume 17 of CCIS, 604-618.
2007
J. Barnat and L. Brim and P. Simecek:
I/O Efficient Accepting Cycle Detection [bibtex, pdf] Computer Aided Verification, Springer, 2007, volume 4590 of LNCS, 281--293.
Jiri Barnat and Lubos Brim and Martin Leucker:
Parallel Model Checking and the FMICS-jETI Platform [bibtex, pdf] The Twelfth IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2007), IEEE Computer Society Press, 2007.
J. Barnat and L. Brim and I. Cerna and S. Drazan and D.Safranek:
Parallel Model-Checking Genetic Regulatory Networks [bibtex, pdf] Towards Systems Biology, Verimag, 2007.
J. Barnat and L. Brim and I. Cerna and M. Ceska and J. Tumova:
ProbDiVinE: A Parallel Qualitative LTL Model Checker [bibtex, pdf] Fourth International Conference on the Quantitative Evaluation of Systems (QEST'07), IEEE Computer Society, 2007, 215-216.
J. Barnat and L. Brim and P. Rockai:
Scalable Multi-core LTL Model-Checking [bibtex, pdf] Model Checking Software, Springer, 2007, volume 4595 of LNCS, 187--203.
L. Brim and J. Barnat:
Tutorial: Parallel Model Checking [bibtex, pdf] Model Checking Software, Springer, 2007, volume 4595 of LNCS, 2--3.
2006
Jiri Barnat and Ivana Cerna:
Distributed Breadth-First Search LTL Model Checking [bibtex, pdf] Special Issue on Parallel and Distributed Databases of Formal Methods in System Design, volume 29(2), September 2006, 117-134(18).
J. Barnat and L. Brim and I. Cerna and P. Moravec and P. Rockai and P. Simecek:
DiVinE -- A Tool for Distributed Verification (Tool Paper) [bibtex, pdf] Computer Aided Verification, Springer Berlin / Heidelberg, 2006, volume 4144/2006 of LNCS, 278-281.
Jiri Barnat and Pavel Moravec:
Parallel Algorithms for Finding SCCs in Implicitly Given Graphs [bibtex, pdf] Formal Methods: Applications and Technology, Springer, 2006, volume 4346 of LNCS, 316--330.
2005
J. Barnat and L. Brim and I. Cerna:
Cluster-Based LTL Model Checking of Large Systems [bibtex, pdf] Formal Methods for Components and Objects, 2005, LNCS, 259-279.
J. Barnat and L. Brim and I. Cerna and P. Simecek:
DiVinE -- The Distributed Verification Environment [bibtex, pdf] Proceedings of 4th International Workshop on Parallel and Distributed
Methods in verifiCation, 2005, 89--94.
J. Barnat and V. Forejt and M. Leucker and M. Weber:
DivSPIN -- A SPIN compatible distributed model checker [bibtex, pdf] Proceedings of 4th International Workshop on Parallel and Distributed
Methods in verifiCation, 2005, 95--100.
J. Barnat and L. Brim and J. Chaloupka:
From Distributed Memory Cycle Detection to Parallel LTL Model
Checking [bibtex, pdf] Electronic Notes in Theoretical Computer Science, volume 133(1), 2005, 21--39.
2004
Jiri Barnat:
Distributed Memory LTL Model Checking [bibtex, pdf]
Ph.D. Thesis, Masaryk University Brno, Faculty of Informatics, 2004.
2003
L. Brim and J. Barnat:
Distribution of Explicit-State LTL
Model-Checking [bibtex, pdf] 8th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 03), Elsevier, 2003, volume 80 of Electronic Notes in Theoretical Computer Science.
J. Barnat and L. Brim and J. Chaloupka:
Parallel Breadth-First Search LTL
Model-Checking [bibtex, pdf] 18th IEEE International Conference on Automated Software
Engineering (ASE'03), IEEE Computer Society, 2003, 106--115.
2002
J. Barnat:
How to Distribute LTL Model-checking Using Decomposition of Negative Claim Automaton [bibtex, pdf] SOFSEM 2002 Student Research Forum, 2002, 9--14.
J. Barnat and L. Brim and I. Cerna:
Property driven distribution of Nested DFS [bibtex, pdf] Proc. Workshop on Verification and Computational Logic, 2002, DSSE Technical Report, 1 - 10.
2001
J. Barnat and L. Brim and J.
Stribrna:
Distributed LTL Model-Checking
in SPIN [bibtex, pdf] Proc. SPIN Workshop on Model Checking of Software, Springer, 2001, volume 2057 of LNCS, 200 - 216.