Research Project Results
Techniques for automatic verification and validation of software nad hardware systems
| Project Identification: | 1ET408050503 |
| MU Investigator: | Prof. RNDr. Luboš Brim, CSc. |
| MU Faculty/Unit: | Faculty of Informatics |
| Project Period: | 1/2005 - 12/2009 |
| Investor/Programme: | Academy of Sciences of the Czech Republic - |
Results: (Czech only)
Teoreticko-metodologické zázemí modelování rozsáhlých systémů. Návrh, analýza a implementace technik pro počítačem podporovanou i automatickou verifikaci a validaci systémů se zaměřením na zapouzdřené, paralelní a distribuované komponenty.
Publications:
BARNAT, Jiří - BRIM, Luboš - ROČKAI, Petr.
On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties. Science of Computer Programming, , Elsevier. ISSN 0167-6423, 2012, vol. 2011, no. 0.
BARNAT, Jiří - CHALOUPKA, Jakub - VAN DE POL, Jaco.
Distributed Algorithms for SCC Decomposition. Journal of Logic and Computation, , Oxford University Press, Great Britain. ISSN 0955-792X, 2011, vol. 21, no. 1, pp. 23-44.
EDELKAMP, Stefan - SULEWSKI, Damian - BARNAT, Jiří - BRIM, Luboš - ŠIMEČEK, Pavel.
Flash memory efficient LTL model checking. Science of Computer Programming, , Elsevier, The Nederlands. ISSN 0167-6423, 2011, vol. 76, no. 2, pp. 136--157.
BARNAT, Jiří - BRIM, Luboš - ROČKAI, Petr.
Scalable shared memory LTL model checking. International Journal on Software Tools for Technology Transfer (STTT), , Springer-Verlag GmbH, Germany. ISSN 1433-2779, 2010, vol. 12, no. 2, pp. 139-153.
BARNAT, Jiří - BRIM, Luboš - ROČKAI, Petr.
A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties. In Formal Methods and Software Engineering. Germany : Springer Berlin / Heidelberg, 2009. ISBN 978-3-642-10372-8, pp. 407-425. 2009, Rio de Janeiro.
BARNAT, Jiří - DRAŽAN, Sven - FABRIKOVÁ, Jana - ŠAFRÁNEK, David - BRIM, Luboš - ČERNÁ, Ivana - LÁNÍK, Jan.
BioDiVinE. 2009.
BARNAT, Jiří - BRIM, Luboš - ČERNÁ, Ivana - DRAŽAN, Sven - FABRIKOVÁ, Jana - LÁNÍK, Jan - ŠAFRÁNEK, David - HONGWU, Ma.
BioDiVinE: A Framework for Parallel Analysis of Biological Models. In Proceedings of 2nd International Workshop on Computational Models for Cell Processes. Neuveden : EPTCS, 2009. pp. 31-45. 2009, Eindhoven.
BARNAT, Jiří - BRIM, Luboš - ČERNÁ, Ivana - DRAŽAN, Sven - FABRIKOVÁ, Jana - LÁNÍK, Jan - ŠAFRÁNEK, David.
BioDiVinE: A Tool for Parallel Analysis of Multi-Affine ODE Models. In Computational Mehotds in Systems Biology: Abstract of the Posters. Pisa : University of Pisa, 2009. pp. 1-5. 2009, Bologna.
BARNAT, Jiří - BRIM, Luboš - EDELKAMP, Stefan - SULEWSKI, Damian - ŠIMEČEK, Pavel.
Can Flash Memory Help in Model Checking?. In Formal Methods for Industrial Critical Systems. Neuveden : Springer Berlin / Heidelberg, 2009. ISBN 978-3-642-03239-4, pp. 150-165. 2008, L'Aquila, Italy.
BARNAT, Jiří - BRIM, Luboš - ŠIMEČEK, Pavel.
Cluster-Based I/O-Efficient LTL Model Checking. In 24th IEEE/ACM International Conference on Automated Software Engineering. Los Calamitos (California) : IEEE Computer Society, 2009. ISBN 978-0-7695-3891-4, pp. 635-639. 2009, Auckalnd, New Zealand.
BARNAT, Jiří - BRIM, Luboš - ČERNÁ, Ivana - DRAŽAN, Sven - FABRIKOVÁ, Jana - ŠAFRÁNEK, David.
Computational Analysis of Large-Scale Multi-Affine ODE Models. In International Workshop on High Performance Computational Systems Biology. Los Alamitos (California) : IEEE Computer Society, 2009. ISBN 978-0-7695-3809-9, pp. 81-90. 2009, Trento.
BARNAT, Jiří - BRIM, Luboš - ČEŠKA, Milan - LAMR, Tomáš.
CUDA Accelerated LTL Model Checking. In Proceedings of the 15th International Conference on Parallel and Distributed Systems. Neuveden : Roy Sterritt, 2009. ISBN 978-0-7695-3900-3, pp. 34-41. 8.12.2009, Shezhen, Čína.
ROČKAI, Petr - BARNAT, Jiří - BRIM, Luboš - ČEŠKA, Milan.
DiVinE 2.0. 2009.
BARNAT, Jiří - BRIM, Luboš - ROČKAI, Petr.
DiVinE 2.0: High-Performance Model Checking. In International Workshop on High Performance Computational Systems Biology. Los Alamitos (California) : IEEE Computer Society, 2009. ISBN 978-0-7695-3809-9, pp. 31-32. 2009, Trento.
BARNAT, Jiří - BRIM, Luboš - BAUCH, Petr - ČEŠKA, Milan - LAMR, Tomáš.
DiVinE Cuda. 2009.
BARNAT, Jiří - BRIM, Luboš - ČEŠKA, Milan.
DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking. Electronic Proceedings in Theoretical Computer Science, , , The Nederlands. ISSN 2075-2180, 2009, vol. 14, no. Prosinec, pp. 107--111.
BENEŠ, Nikola - KŘETÍNSKÝ, Jan - LARSEN, Kim G. - SRBA, Jiří.
Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete. In Theoretical Aspects of Computing - ICTAC 2009, 6th International Colloquium, Kuala Lumpur, Malaysia, August 16-20, 2009. Proceedings. Heidelberg : Springer-Verlag, 2009. ISBN 978-3-642-03465-7, pp. 112-126. 2009, Kuala Lumpur.
BARNAT, Jiří - BRIM, Luboš - ČERNÁ, Ivana - ČEŠKA, Milan - TŮMOVÁ, Jana.
Local Quantitative LTL Model Checking. In Formal Methods for Industrial Critical Systems. Neuveden : Springer Berlin / Heidelberg, 2009. ISBN 978-3-642-03239-4, pp. 53-68. 2008, L'Aquila, Italy.
ŠAFRÁNEK, David.
On Computational Analysis of Large ODE Models. 2009.
KŘETÍNSKÝ, Mojmír - ŘEHÁK, Vojtěch - STREJČEK, Jan.
On Decidability of LTL+Past Model Checking for Process Rewrite Systems. In Joint Proceedings of the 8th, 9th, and 10th International Workshops on Verification of Infinite-State Systems (INFINITY 2006, 2007, 2008). Vyd. 2009. Amsterdam, The Netherlands : Elsevier Science Publishers, 2009. pp. 105-117. 2007, Lisbon, Portugal.
BENEŠ, Nikola - BRIM, Luboš - ČERNÁ, Ivana - SOCHOR, Jiří - VAŘEKOVÁ, Pavlína - ZIMMEROVÁ, Barbora.
Partial Order Reduction for State/Event LTL. In Proceedings of the International Conference on Integrated Formal Methods (IFM'09). Berlin / Heidelberg, Germany : Springer Verlag, 2009. ISBN 978-3-642-00254-0, pp. 307-321. 16.2.2009, Düsseldorf, Germany.
KŘETÍNSKÝ, Mojmír - ŘEHÁK, Vojtěch - STREJČEK, Jan.
Reachability is decidable for weakly extended process rewrite systems. Information and Computation, , Elsevier, USA. ISSN 0890-5401, 2009, vol. 207, no. 6, pp. 671-680.
BENEŠ, Nikola - ČERNÁ, Ivana - SOCHOR, Jiří - MORAVCOVÁ VAŘEKOVÁ, Pavlína - BÜHNOVÁ, Barbora.
A Case Study in Parallel Verification of Component-Based Systems. Electronic Notes in Theoretical Computer Science, Neuveden, Elsevier, Hungary. ISSN 1571-0661, 2008, vol. 220, no. 2, pp. 67-83.
BENEŠ, Nikola - ČERNÁ, Ivana - SOCHOR, Jiří - VAŘEKOVÁ, Pavlína - ZIMMEROVÁ, Barbora.
A Case Study in Parallel Verification of Component-Based Systems. In Pre-proceedings of the Workshop on Parallel and Distributed Methods in verifiCation (PDMC'08). Budapest, Hungary : ETAPS, 2008. pp. 35-51. 29.3.2008, Budapest, Hungary.
MORAVCOVÁ VAŘEKOVÁ, Pavlína - VAŘEKOVÁ, Ivana - ČERNÁ, Ivana.
Automated Computing of the Maximal Number of Handled Clients for Client-Server Systems. In Proceedings of the International Workshop on Formal Aspects of Component Software (FACS'08). Málaga, Spain : Department of Computer Science, University of Málaga, 2008. pp. 41-55. 10.9.2008, Málaga, Spain.
BARNAT, Jiří - BRIM, Luboš - EDELKAMP, Stefan - SULEWSKI, Damian - ŠIMEČEK, Pavel.
Can Flash Memory Help in Model Checking?. In 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008). L'Aquilla : ERCIM, 2008. pp. 159-174. 2008, L'Aquilla.
ZIMMEROVÁ, Barbora - VAŘEKOVÁ, Pavlína - BENEŠ, Nikola - ČERNÁ, Ivana - BRIM, Luboš - SOCHOR, Jiří.
Component-Interaction Automata Approach (CoIn). In The Common Component Modeling Example: Comparing Software Component Models. Berlin / Heidelberg, Germany : Springer Verlag, 2008. LNCS 5153, ISBN 978-3-540-85288-9, pp. 146-176.
BARNAT, Jiří - BRIM, Luboš - ČERNÁ, Ivana - ČEŠKA, Milan - ŠIMEČEK, Pavel.
DiVinE Cluster. 2008.
BARNAT, Jiří - BRIM, Luboš - ROČKAI, Petr.
DiVinE Multi-Core -- A Parallel LTL Model-Checker. In Automated Technology for Verification and Analysis. Berlin / Heidelberg : Springer, 2008. ISBN 978-3-540-88386-9, pp. 234-239. 2008, Seoul.
ŠIMEČEK, Pavel - PELÁNEK, Radek.
Estimating State Space Parameters. 2008.
VAŘEKOVÁ, Pavlína - ZIMMEROVÁ, Barbora - MORAVEC, Pavel - ČERNÁ, Ivana.
Formal verification of systems with an unlimited number of components. IET Software journal, , Inst. of Engeneering and Technology, USA. ISSN 1751-8806, 2008, vol. Volume 2, no. Isuue 6, pp. p. 532-546.
BARNAT, Jiří - BRIM, Luboš - ČERNÁ, Ivana - DRAŽAN, Sven - ŠAFRÁNEK, David.
From Simple Regulatory Motifs to Parallel Model Checking of Complex Transcriptional Networks. In Proceedings of PDMC 2008 - Parallel and Distributed Methods ins VerifiCation. Budapest : Ivana Cerna and Gerald Luettgen, 2008. pp. 83-96. 2008, Budapest.
DRAŽAN, Sven - ŠAFRÁNEK, David - BARNAT, Jiří.
GeNeSim: Genetic Network Simulator GUI. 2008.
ŠIMEČEK, Pavel.
I/O Efficient Model Checking. 2008.
BARNAT, Jiří - CHALOUPKA, Jakub - VAN DE POL, Jaco.
Improved Distributed Algorithms for SCC Decomposition. Electronic Notes in Theoretical Computer Science, , Elsevier, The Nederlands. ISSN 1571-0661, 2008, vol. 2008, no. 198(1), pp. 63-77.
BARNAT, Jiří - BRIM, Luboš - ČERNÁ, Ivana - ČEŠKA, Milan - TŮMOVÁ, Jana.
Local Quantitative LTL Model Checking. In 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008). L'Aquilla : ERCIM, 2008. ISBN 978-3-642-03239-4, pp. 63-78. 2008, L'Aquilla.
MORAVCOVÁ VAŘEKOVÁ, Pavlína - ČERNÁ, Ivana.
Model Checking of Control-User Component-Based Parametrised Systems. In Lecture Notes in Computer Science 5282. Germany : Springer Verlag, 2008. ISBN 978-3-540-87890-2, pp. 146-162. 2008, Karlsruhe.
ŠAFRÁNEK, David.
On Algorithmic Analysis of Biological Networks. 2008.
BARNAT, Jiří - BRIM, Luboš - ČERNÁ, Ivana - DRAŽAN, Sven - ŠAFRÁNEK, David.
Parallel Model Checking Large-Scale Genetic Regulatory Networks with DiVinE. In Electronic Notes in Theoretical Computer Science. Vyd. Vol. 194/3. Elsevier : Elsevier Science, 2008. pp. 35-50. 2007, LisbonProceedings of From Biology to Concurrency and Back (FBTC 2007).
BENEŠ, Nikola - BRIM, Luboš - ČERNÁ, Ivana - SOCHOR, Jiří - VAŘEKOVÁ, Pavlína - ZIMMEROVÁ, Barbora.
Partial Order Reduction for State/Event LTL. Brno, Czech Republic : Faculty of Informatics, Masaryk University, 2008. Technical report FIMU-RS-2008-07.
KŘETÍNSKÝ, Mojmír - ŘEHÁK, Vojtěch - STREJČEK, Jan.
Petri Nets Are Less Expressive Than State-Extended PA. Theoretical Computer Science, Amsterdam, North Holland, Elsevier Science Publishers, The Nederlands. ISSN 0304-3975, 2008, vol. 394, no. 1-2, pp. 134-140. DOI 10.1016/j.tcs.2007.12.003.
BARNAT, Jiří - BRIM, Luboš - ČERNÁ, Ivana - ČEŠKA, Milan - TŮMOVÁ, Jana.
ProbDiVinE-MC. 2008.
BARNAT, Jiří - BRIM, Luboš - ČERNÁ, Ivana - ČEŠKA, Milan - TŮMOVÁ, Jana.
ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems. In QEST '08: Proceedings of the 2008 Fifth International Conference on Quantitative Evaluation of Systems. Washington, DC, USA : IEEE Computer Society, 2008. ISBN 978-0-7695-3360-5, pp. 77-78. 2008, St Malo, France.
BARNAT, Jiří - BRIM, Luboš - ŠIMEČEK, Pavel - WEBER, Michael.
Revisiting Resistance Speeds Up I/O Efficient LTL Model Checking. In Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg : Springer-Verlag, 2008. ISBN 978-3-540-78799-0, pp. 48-62. 2008, Budapest, Hungary.
EDELKAMP, Stefan - SANDERS, Peter - ŠIMEČEK, Pavel.
Semi-external LTL Model Checking. In 20th International Conference on Computer Aided Verification. Berlin, Heidelberg : Springer, 2008. ISBN 978-3-540-70543-7, pp. 530-542.
ŠIMEČEK, Pavel.
Semi-External LTL Model Checking. Co-authors of the original paper in CAV 2008 proceedings. 2008.
BARNAT, Jiří - ROČKAI, Petr.
Shared Hash Tables in Parallel Model Checking. Electronic Notes in Theoretical Computer Science, , Elsevier, The Nederlands. ISSN 1571-0661, 2008, vol. 2008, no. 198(1), pp. 79-91.
BARNAT, Jiří - BRIM, Luboš.
Squeeze All the Power Out of Your Hardware to Verify Your Software!. In Leveraging Applications of Formal Methods, Verification and Validation. Berlin Heidelberg : Springer, 2008. ISBN 978-3-540-88478-1, pp. 604-618.
BENEŠ, Nikola - BRIM, Luboš - ČERNÁ, Ivana - SOCHOR, Jiří - VAŘEKOVÁ, Pavlína - ZIMMEROVÁ, Barbora.
The CoIn Tool: Modelling and Verification of Interactions in Component-Based Systems. In Pre-proceedings of the International Workshop on Formal Aspects of Component Software (FACS'08). Málaga, Spain : Department of Computer Science, University of Málaga, 2008. pp. 221-225. 10.9.2008, Málaga, Spain.
ČERNÁ, Ivana - VAŘEKOVÁ, Pavlína - ZIMMEROVÁ, Barbora.
Component Substitutability via Equivalencies of Component-Interaction Automata. Electronic Notes in Theoretical Computer Science, , Elsevier, The Nederlands. ISSN 1571-0661, 2007, vol. 182, no. 1, pp. 39-55.
BARNAT, Jiří - BRIM, Luboš - ROČKAI, Petr.
DiVinE Multi-Core. 2007.
VAŘEKOVÁ, Pavlína - MORAVEC, Pavel - ČERNÁ, Ivana - ZIMMEROVÁ, Barbora.
Effective verification of systems with a dynamic number of components. In 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. New York, NY, USA : ACM Press, 2007. ISBN 978-1-59593-721-6, pp. 3-13. 3.9.2007, Dubrovnik, Croatia.
BABICA, Jindřich - ŘEHÁK, Vojtěch - SLOVÁK, Petr - TROUBIL, Pavel - ZAVADIL, Martin.
Formalisms and Tools for Design and Specification of Network Protocols. Brno : FI MU, 2007. FIMU-RS-2007-02. 
WWW.
BARNAT, Jiří - BRIM, Luboš - ŠIMEČEK, Pavel.
I/O Efficient Accepting Cycle Detection. In 19th International Conference on Computer Aided Verification. Berlin, Heidelberg : Springer, 2007. ISBN 978-3-540-73367-6, pp. 281-293.
BARNAT, Jiří - CHALOUPKA, Jakub - VAN DE POL, Jaco.
Improved Distributed Algorithms for SCC Decomposition. CTIT Workshop Proceedings, University of Twente, CTIT, Germany. ISSN 0929-0672, 2007, vol. 2007, no. WP 07-04, pp. 65-80.
BRIM, Luboš - KŘETÍNSKÝ, Mojmír.
Model Checking Large Finite-State Systems and Beyond. In 33rd Conference on Current Trends in Theory and Practice of Computer Science. Berlin : Springer-Verlag, 2007. ISBN 978-3-540-69506-6, pp. 9-28. 2007, Harrachov.
KŘETÍNSKÝ, Mojmír - ŘEHÁK, Vojtěch - STREJČEK, Jan.
On Decidability of LTL+Past Model Checking for Process Rewrite Systems. 2007.
BARNAT, Jiří - MORAVEC, Pavel.
Parallel Algorithms for Finding SCCs in Implicitly Given Graphs. In Formal Methods: Applications and Technology. Berlin, Heidelberg : Springer-Verlag, 2007. ISBN 978-3-540-70951-0, pp. 316-330. 2006, Bonn, Germany.
BARNAT, Jiří - BRIM, Luboš - ČERNÁ, Ivana - DRAŽAN, Sven - ŠAFRÁNEK, David.
Parallel Analysis of Genetic Regulatory Networks. 2007.
BARNAT, Jiri - BRIM, Lubos - LEUCKER, Martin.
Parallel Model Checking and the FMICS-jETI Platform. In Proceedings Twelfth IEEE International Conference on Engineering of Complex Computer Systems. Los Alamitos : IEEE Computer Society, 2007. ISBN 0-7695-2895-3, pp. 330-339. 2007, The University of Auckland, New Zealand.
BARNAT, Jiří - BRIM, Luboš - ČERNÁ, Ivana - DRAŽAN, Sven - ŠAFRÁNEK, David.
Parallel Model Checking Large-Scale Genetic Regulatory Networks with DiVinE. In Preproceedings of the Workshop From Biology to Concurrency and Back. Lisbon : Complex System Research Group, University of Camerino, 2007. pp. 80-95. 2007, Lisbon.
BARNAT, Jiří - BRIM, Luboš - ČERNÁ, Ivana - ČEŠKA, Milan - TŮMOVÁ, Jana.
ProbDiVinE. 2007.
BARNAT, Jiří - BRIM, Luboš - ČERNÁ, Ivana - ČEŠKA, Milan - TŮMOVÁ, Jana.
ProbDiVinE: A Parallel Qualitative LTL Model Checker. In Fourth International Conference on the Quantitative Evaluation of Systems (QEST'07). United States of America : IEEE Computer Society, 2007. ISBN 0-7695-2883-X, pp. 215-216. 2007, Edinburgh, Scotland.
MORAVEC, Pavel - ŠIMŠA, Jiří.
Relaxed Cycle Condition Improves Partial Order Reduction. In 3rd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2007). Znojmo, Czech Republic : FI MU, FIT VUT, 2007. ISBN 978-80-7355-077-6, pp. 140-147. 2007, Znojmo, Czech Republic.
BARNAT, Jiří - BRIM, Luboš - ROČKAI, Petr.
Scalable Multi-core LTL Model-Checking. In Model Checking Software. Vyd. 1. Berlin, Heidelberg : Springer-Verlag, 2007. ISBN 978-3-540-73369-0, pp. 187-203. 2007, Berlin, Germany.
BARNAT, Jiří - ROČKAI, Petr.
Shared Hash Tables in Parallel Model Checking. CTIT Workshop Proceedings, University of Twente, CTIT, Germany. ISSN 0929-0672, 2007, vol. 2007, no. WP 07-04, pp. 81-95.
SMRČKA, Aleš - ŘEHÁK, Vojtěch - VOJNAR, Tomáš - ŠAFRÁNEK, David - MATOUŠEK, Petr - ŘEHÁK, Zdeněk.
Verifying VHDL Designs with Multiple Clocks in SMV. In Formal Methods Applications and Technology, 11th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2006, and 5th International Workshop on Parallel and Distributed Methods in Verification, PDMC 2006. Bonn : Springer-Verlag, 2007. ISBN 978-3-540-70951-0, pp. 148-164.
BRIM, Luboš - LEUCKER, Martin.
11th International Workshop on Formal Methods for Industrial Critical Systems. 2006. Federal Republic of Germany, Bonn, Germany. 26.8.2006 - 27.8.2006, Worldwide Activity.
ŠAFRÁNEK, David.
Architectural Interoperability Checking in Visual Coordination Networks. In Combined Proceedings of the Second International Workshop on Coordination and Organization (CoOrg 2006) and the Second International Workshop on Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems (MTCoord 2006). Bologna : Elsevier Science, 2006. pp. 81-96. 2006, Bolognavol. 181.
BARNAT, Jiří - BRIM, Luboš - ČERNÁ, Ivana.
Cluster-Based LTL Model Checking of Large Systems. In Formal Methods for Components and Objects. Berlin : Springer, 2006. ISBN 978-3-540-36749-9, pp. 259-279. 2006, Amsterdam.
ČERNÁ, Ivana - VAŘEKOVÁ, Pavlína - ZIMMEROVÁ, Barbora.
Component Substitutability via Equivalencies of Component-Interaction Automata. In Pre-proceedings of the International Workshop on Formal Aspects of Component Software (FACS'06). Macao : UNU-IIST, 2006. pp. 115-130. 20.9.2006, Prague, Czech Republic.
BARNAT, Jiří - ČERNÁ, Ivana.
Distributed breadth-first search LTL model checking. Formal Methods in System Design, , Springer Netherlands, The Nederlands. ISSN 0925-9856, 2006, vol. 29, no. 2, pp. 117-134.
BARNAT, Jiří - BRIM, Luboš - ČERNÁ, Ivana - ČEŠKA, Milan - TŮMOVÁ, Jana.
Distributed Qualitative LTL Model Checking of Markov Decision Processes. In Proceedings of 5th International Workshop on Parallel and Distributed Methods in verifiCation. Bonn, Germany : University of Bonn, 2006. pp. 1-15. 2006, Bonn.
BRIM, Luboš.
Distributed Verification: Exploring the Power of Raw Computing Power. In 5th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2006). Bonn, Germany : TU Munchen, 2006. ISBN 3-540-70951-7, pp. 23-34. 2006, Bonn, Germany.
BARNAT, Jiří - BRIM, Luboš - ČERNÁ, Ivana - MORAVEC, Pavel - ROČKAI, Petr - ŠIMEČEK, Pavel.
DiVinE -- A Tool for Distributed Verification. In Computer Aided Verification. Berlin : Springer Verlag, 2006. ISBN 978-3-540-37406-0, pp. 278-281. Seatle, WA, USA.
BARNAT, Jiří - BRIM, Luboš - ČERNÁ, Ivana - MORAVEC, Pavel - ŠIMEČEK, Pavel - CHALOUPKA, Jakub.
DiVinE Library. 2006.
MORAVEC, Pavel.
Experimental Comparison of Algorithms Checking Proviso for Partial Order Reduction. In 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006). Mikulov, Czech Republic : FI MU Report Series, 2006. pp. 129-136. 2006, Mikulov, Czech Republic.
KRATOCHVÍLA, Tomáš - ŘEHÁK, Vojtěch - ŠAFRÁNEK, David.
Formal Verification of a FIFO Component in Design of Network Monitoring Hardware. In 10 years of CESNET - CESNET CONFERENCE 2006. Praha : CESNET, z.s.p.o., 2006. ISBN 978-80-239-6533-9, pp. 151-160. 2006, Praha.
BRIM, Luboš - ČERNÁ, Ivana - MORAVEC, Pavel - ŠIMŠA, Jiří.
How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors. Electronic Notes in Theoretical Computer Science, Nizozemsko, Elsevier, Portugal. ISSN 1571-0661, 2006, vol. 135, no. 2, pp. 3-18.
ČERNÁ, Ivana - BRÁZDIL, Tomáš.
Model Checking of RegCTL. Computing and Informatics, , , Slovakia. ISSN 1335-9150, 2006, vol. 25, no. 1, pp. 81-97.
ŠIMŠA, Jiří.
On Alternative Construction of LTL Tableau. In 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006). Mikulov, Czech Republic : FI MU Report Series, 2006. pp. 222-229. 2006, Mikulov, Czech Republic.
BRIM, Luboš - ČERNÁ, Ivana - MORAVEC, Pavel - ŠIMŠA, Jiří.
On Combining Partial Order Reduction with Fairness Assumptions. In Proceedings of the 11th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2006). Bonn, Germany : University Bonn, 2006. ISBN 978-3-540-70951-0, pp. 1-16. 2006, Bonn, Germany.
BOZZELLI, Laura - KŘETÍNSKÝ, Mojmír - ŘEHÁK, Vojtěch - STREJČEK, Jan.
On Decidability of LTL Model Checking for Process Rewrite Systems. In FSTTCS 2006: 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings. Berlin : Springer-Verlag, 2006. ISBN 978-3-540-49994-7, pp. 248-259. 2006, Kolkata, IndiaLecture Notes in Computer Science 4337.
BOZZELLI, Laura - KŘETÍNSKÝ, Mojmír - ŘEHÁK, Vojtěch - STREJČEK, Jan.
On Decidability of LTL Model Checking for Weakly Extended Process Rewrite Systems. Brno : FI MU, 2006. FIMU-RS-2006-05. full and extended version of FST&TCS'06 paper. WWW.
BARNAT, Jiří - MORAVEC, Pavel.
Parallel Algorithms for Finding SCCs in Implicitly Given Graphs. In Proceedings of the 5th International Workshop on
Proceedings of 5th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2006). Bonn, Germany : University Bonn, 2006. pp. 20-34. 2006, Bonn, Germany.
KŘETÍNSKÝ, Mojmír - ŘEHÁK, Vojtěch - STREJČEK, Jan.
Refining Undecidability Border of Weak Bisimilarity. In Proceedings of the 7th International Workshop on Verification of Infinite-State Systems (INFINITY'05). Vyd. 2006. Amsterdam, The Netherlands : Elsevier Science, 2006. pp. 17-36. 2005, San Francisco, USAmodified and extended version of INFINITY 2005 paper.
ANTOŠ, David - ŘEHÁK, Vojtěch.
Routing and Level 2 Addressing in a Hardware Accelerator for Network Applications. In ICT 2006, 13th International Conference on Telecommunications. Funchal, Madeira : University of Aveiro, Portugal, 2006. ISBN 972-98368-4-1, pp. 1-4. 8.5.2005, Funchal, Portugal.
BRIM, Luboš - LEUCKER, Martin.
Special Issue on Parallel and Distributed Verification - Foreword. Formal Methods in System Design, , Springer Netherlands, The Nederlands. ISSN 0925-9856, 2006, vol. 29, no. 2, pp. 115-116.
PELÁNEK, Radek - PASAREANU, Corina - VISSER, Willem.
Test Input Generation for Java Containers using State Matching. In International Symposium on
International Symposium on Software Testing and Analysis. USA : ACM, 2006. ISBN 1-59593-263-1, pp. 37--48. 2006, Portland, Maine.
ŘEHÁK, Vojtěch.
Weakly Extended Process Rewrite Systems. 2006.
PELÁNEK, Radek - PASAREANU, Corina - VISSER, Willem.
Concrete Search with Abstract Matching and Refinement. In Computer Aided Verification. Edinburgh : Springer, 2005. ISBN 3-540-27231-3, pp. 52-66. 2005, Edinburgh.
ŠAFRÁNEK, David - ŘEHÁK, Vojtěch - KRATOCHVÍLA, Tomáš - ŠIMEČEK, Pavel - HLÁVKA, Petr - VOJNAR, Tomáš.
CRC64 Algorithm Analysis and Verification. Brno : CESNET, z. s. p. o., 2005. Technical Report 27/2005. WWW.
BARNAT, Jiří - BRIM, Luboš - ČERNÁ, Ivana.
Distributed Analysis of Large Systems. In Formal Methods for Components and Objects. Amsterdam : CWI Amsterdam, 2005. pp. 31-35. 2005, Amsterdam.
BARNAT, Jiří - BRIM, Luboš - ČERNÁ, Ivana - ŠIMEČEK, Pavel.
DIVINE - The Distributed Verification Environment. In In proceedings of 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC05). Lisboa, Portugal : TU Munchen, 2005. pp. 89-94. 2005, Lisboa, Portugalsko.
BARNAT, Jiří - FOREJT, Vojtěch - LEUCKER, Martin - WEBER, Michael.
DivSPIN - A SPIN compatible distributed model checker. In Proceedings of 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC05). Lisabon, Portugalsko : TU Munchen, 2005. pp. 95-100. 2005, Lisabon, Portugalsko.
PELÁNEK, Radek - HANŽL, Tomáš - ČERNÁ, Ivana - BRIM, Luboš.
Enhancing Random Walk State Space Exploration. In Formal Methods for Industrial Critical Systems. Lisbon : ACM SIGSOFT, 2005. ISBN 1-59593-148-1, pp. 98-105. 2005, Lisbon.
BRIM, Luboš - ČERNÁ, Ivana - MORAVEC, Pavel - ŠIMŠA, Jiří.
How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors. In Proceedings of the 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2005). Lisboa, Portugal : TU Munchen, 2005. pp. 1-12. 2005, Lisboa, Portugal.
BRIM, Luboš - LINDEN, Isabelle.
MTCoord 2005 1st International Workshop on Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems. 2005. Kingdom of Belgium, Namur, Belgie. 23.4.2005 - 23.4.2005, Worldwide Activity.
PELÁNEK, Radek - KRČÁL, Pavel.
On Sampled Semantics of Timed Systems. In Foundations of Software Technology and Theoretical Computer Science. India : Springer, 2005. ISBN 978-3-540-30495-1, pp. 310-321. Hyderabad.
KŘETÍNSKÝ, Mojmír - ŘEHÁK, Vojtěch - STREJČEK, Jan.
Reachability of Hennessy - Milner properties for weakly extended PRS. In FSTTCS 2005: 25th International Conference on Foundations of Software Technology and Theoretical Computer Science, 25th International Conference. Berlin, Heidelberg : Springer-Verlag, 2005. ISBN 3-540-30495-9, pp. 213-224. 2005, Hyderabad, India.
KŘETÍNSKÝ, Mojmír - ŘEHÁK, Vojtěch - STREJČEK, Jan.
Refining Undecidability Border of Weak Bisimilarity. BRICS Notes Series, San Francisco, USA, . ISSN 0909-3206, 2005, vol. 2005, no. NS-05-4, pp. 3-14.
KŘETÍNSKÝ, Mojmír - ŘEHÁK, Vojtěch - STREJČEK, Jan.
Refining Undecidability Border of Weak Bisimilarity. (full version of INFINITY 2005 paper). Brno : FI MU, 2005. FIMU-RS-2005-06. WWW.
KUČERA, Antonín - STREJČEK, Jan.
The stuttering principle revisited. Acta informatica, Berlin, Springer-Verlag, Germany. ISSN 0001-5903, 2005, vol. 41, no. 7/8, pp. 415-434.
