Skip to main content.

Publications



2009


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, 2009, volume 5596 of LNCS, 150--165.


J. Barnat and J. Chaloupka and J. Van De Pol: Distributed Algorithms for SCC Decomposition [bibtex, pdf]
To appear in Journal of Logic and Computation, volume , 2009, .


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 M. Ceska and J. Tumova: Local Quantitative LTL Model Checking [bibtex, pdf]
Formal Methods for Industrial Critical Systems (FMICS 2008), Springer-Verlag, 2009, volume 5596 of LNCS, 53--68.



2008


J. Barnat and L. Brim and P. Rockai: DiVinE Multi-Core -- A Parallel LTL Model-Checker [bibtex, pdf]
Automated Technology for Verification and Analysis, Springer, 2008, volume 5311 of LNCS, 234-239.


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, month), 2005, 21--39.


L. Brim and I. Cerna and P. Moravec and J. Simsa: How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors [bibtex, pdf]
4rd International Workshop on Parallel and Distributed Methods in verifiCation, 2005.



2004


L. Brim and I. Cerna and P. Moravec and J. Simsa: Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking [bibtex, pdf]
5th International Conference on Formal Methods in Computer-Aided Design (FMCAD'04), Springer-Verlag, 2004, volume 3312 of LNCS, 352-366.


Jiri Barnat: Distributed Memory LTL Model Checking [bibtex, pdf]
Ph.D. Thesis, Masaryk University Brno, Faculty of Informatics, 2004.


Lubos Brim and Ivana Cerna and Lukas Hejtmanek: Distributed Negative Cycle Detection Algorithms [bibtex, pdf]
Parallel Computing: Software Technology, Algorithms, and Applications (PARCO'03), Elsevier, 2004, volume 13 of Advances in Parallel Computing, 297--304.


L. Brim and I. Cerna and P. Moravec and J. Simsa: Distributed Partial Order Reduction of State Spaces [bibtex, pdf]
3rd International Workshop on Parallel and Distributed Methods in verifiCation, 2004.



2003


I. Cerna and R. Pelanek: Distributed Explicit Fair Cycle Detection [bibtex, pdf]
Proc. SPIN workshop, Springer, 2003, volume 2648 of LNCS, 49-74.


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 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


L. Brim and I. Cerna and P. Krcal and R. Pelanek: Distributed LTL Model Checking Based on Negative Cycle Detection [bibtex, pdf]
Proc. Foundations of Software Technology and Theoretical Computer Science, Springer, 2001, opteditor, volume 2245, series of , 96--107.


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.