Research Project Results
Automated Verification of Parallel and Distributed Systems
| Project Identification: | GA201/03/0509 |
| MU Investigator: | Prof. RNDr. Luboš Brim, CSc. |
| MU Faculty/Unit: | Faculty of Informatics |
| Project Period: | 1/2003 - 12/2005 |
| Investor/Programme: | Czech Science Foundation / Standard Projects- |
Publications:
HEJTMÁNEK, Lukáš.
Secure and Fault Tolerant Distributed Framework with Mobility Support. In Grid Middleware and Services - Challenges and Solutions. New York, NY, USA : Springer Science + Business Media, 2008. ISBN 978-0-387-78445-8, pp. 289-304. 2008, Dresden, Germany.
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.
PELÁNEK, Radek - LARSEN, Kim G. - BEHRMANN, Gerd - BOUYER, Patricia.
Lower and Upper Bounds in Zone-Based Abstractions of Timed Automata. International Journal on Software Tools for Technology Transfer (STTT), , Springer-Verlag GmbH, Germany. ISSN 1433-2779, 2006, vol. 8, no. 3, pp. 204-215.
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.
BRIM, Luboš - ŽIDKOVÁ, Jitka - YORAV, Karen.
Assumption-based distribution of CTL model checking. International Journal on Software Tools for Technology Transfer (STTT), , Springer-Verlag GmbH, Germany. ISSN 1433-2779, 2005, vol. 7, no. 1, pp. 61-73.
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.
PELÁNEK, Radek - STREJČEK, Jan.
Deeper Connections between LTL and Alternating Automata. In Implementation and Application of Automata. Berlin, Heidelberg : Springer-Verlag, 2005. ISBN 978-3-540-31023-5, pp. 238-249. 2005, Sophia Antipolis.
BRIM, Luboš - ČERNÁ, Ivana - MORAVEC, Pavel - ŠIMŠA, Jiří.
Distributed Partial Order Reduction of State Spaces. Electronic Notes on Theoretical Computer Science, , Elsevier, The Nederlands. ISSN 1571-0661, 2005, vol. 128, no. 3, pp. 63-74.
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.
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.
BARNAT, Jiří - BRIM, Luboš - CHALOUPKA, Jakub.
From Distributed Memory Cycle Detection to Parallel LTL Model Checking. Electronical Notes in Theoretical Computer Science, , Elsevier, The Nederlands. ISSN 1571-0661, 2005, vol. 2005, no. 133, pp. 21-39.
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š - GRUMBERG, Orna.
Introductory paper: Parallel and Distributed Model Checking. International Journal on Software Tools for Technology Transfer (STTT), , Springer-Verlag GmbH, Germany. ISSN 1433-2779, 2005, vol. 7, no. 1, pp. 1-3.
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.
PELÁNEK, Radek - PASAREANU, Corina - VISSER, Willem.
Test input generation for red-black trees using abstraction. In Automated Software Engineering. USA : ACM, 2005. pp. 414-417. 2005, Long Beach, California.
BRIM, Luboš - ČERNÁ, Ivana - MORAVEC, Pavel - ŠIMŠA, Jiří.
Under-Approximation Generation using Partial Order Reduction. Brno : Faculty of Informatics, 2005. 21 s. Technical Reports, FIMU-RS-2005-04.
ŠAFRÁNEK, David - ŠIMŠA, Jiří.
VCD: A Visual Formalism for Specification of Heterogeneous Software Architectures. In SOFSEM 2005: Theory and Practice of Computer Science. Heidelberg : Springer, 2005. ISBN 3-540-24302-X, pp. 320-330. Liptovský Ján.
BRIM, Luboš.
3rd International Workshop on Parallel and Distributed Methods in verifiCation (PDMC'04). 2004. United Kingdom of Great Britain and Northern Ireland, London. 4.9.2004 - 4.9.2004, Worldwide Activity.
BRIM, Luboš - ČERNÁ, Ivana - MORAVEC, Pavel - ŠIMŠA, Jiří.
Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking. In Formal Methods in Computer-Aided Design (FMCAD). Neuveden : Springer-Verlag, LNCS 3312, 2004. ISBN 3-540-23738-0, pp. 352-366. 2004, Austin, USA.
BRIM, Luboš - ČERNÁ, Ivana - MORAVEC, Pavel - ŠIMŠA, Jiří.
Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking. Brno : Faculty of Informatics, 2004. 22 s. Technical Reports, FIMU-RS-2004-09. Full version of the FMCAD'04 paper.
BARNAT, Jiří - BRIM, Luboš - CHALOUPKA, Jakub.
Distributed Memory LTL Model Checking Based on Breadth First Search. Brno : Faculty of Informatics, Masaryk University Brno, 2004. 57 s. FIMU-RS-2004-07.
BRIM, Luboš - ČERNÁ, Ivana - HEJTMÁNEK, Lukáš.
Distributed Negative Cycle Detection Algorithms. In Parallel Computing: Software Technology, Algorithms, Architectures & Applications. Nizozemsko : Elsevier B.V., 2004. ISBN 0-444-51689-1, pp. 297-305. 2003, Dresden.
BRIM, Luboš - ČERNÁ, Ivana - MORAVEC, Pavel - ŠIMŠA, Jiří.
Distributed Partial Order Reduction of State Spaces. In Proceedings of the 3rd International Workshop on Parallel and Distributed Verifationic (PDMC 2004). London, U.K. : Imperial College London, 2004. pp. 3-18. 2004, London, U.K.
BARNAT, Jiří - BRIM, Luboš - CHALOUPKA, Jakub.
From Distributed Memory Cycle Detection to Parallel LTL Model Checking. In Proceedings of the Ninth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2004). Linz, Austria : Institute for Systems Engineering & Automation, Kepler university Linz, 2004. ISBN 3-902457-03-1, pp. 17-34. 2004, Linz, Austria.
ANTOŠ, David - ŘEHÁK, Vojtěch - KOŘENEK, Jan.
Hardware Router's Lookup Machine and its Formal Verification. In ICN'2004 Conference Proceedings. Gosier, Guadeloupe, French Caribbean : University of Haute Alsace, Colmar, France, 2004. ISBN 0-86341-325-0, pp. 1002-1007. 29.2.2004, Gosier, Guadeloupe.
HOLEČEK, Jan - KRATOCHVÍLA, Tomáš - ŘEHÁK, Vojtěch - ŠAFRÁNEK, David - ŠIMEČEK, Pavel.
How to Formalize FPGA Hardware Design. Praha : CESNET, z.s.p.o., 2004. CESNET Technical Report No. 04/2004. WWW.
PELÁNEK, Radek - LARSEN, Kim G. - BEHRMANN, Gerd - BOUYER, Patricia.
Lower and Upper Bounds in Zone Based Abstractions of Timed Automata. In Tools and Algorithms for Construction and Analysis of Systems (TACAS 2004). Barcelona (Španělsko) : Springer-Verlag, 2004. ISBN 3-540-21299-X, pp. 312-326. 2004, Barcelona.
BRIM, Luboš.
Parallel Model-Checking. ERCIM News, , ERCIM EEIG. ISSN 0926-4981, 2004, vol. 58, no. June, pp. 35-36.
PELÁNEK, Radek.
Typical Structural Properties of State Spaces. In SPIN Workshop 2004. Barcelona (Španělsko) : Springer-Verlag, 2004. ISBN 3-540-21314-7, pp. 5-22. 2004, Barcelona.
MORAVEC, Pavel.
Using Accepting Predecessors in Distributed LTL Model-Checking. In MOVEP'04: 6th school on MOdeling and VErifying parallel Processes. Bruxelles, Belgium : Universite Libre de Bruxelles, 2004. pp. 122-129. 2004, Universite Libre de Bruxelles.
HOLEČEK, Jan - KRATOCHVÍLA, Tomáš - ŘEHÁK, Vojtěch - ŠAFRÁNEK, David - ŠIMEČEK, Pavel.
Verification Process of Hardware Design in Liberouter Project. Praha : CESNET z.s.p.o., 2004. CESNET Technical Report No. 05/2004. WWW.
HOLEČEK, Jan - KRATOCHVÍLA, Tomáš - ŘEHÁK, Vojtěch - ŠAFRÁNEK, David - ŠIMEČEK, Pavel.
Verification Results in Liberouter Project. Praha : CESNET, z.s.p.o., 2004. CESNET Technical Report No. 03/2004. WWW.
ŠAFRÁNEK, David.
Visual Coordination Diagrams. In Proceedings of the Doctoral Symposium of 7th International Conference on the Unified Modeling Language. Lisbon, Portugal : Alanen M., Cabot J., Goulao M., Saez J. and Simmonds D. (editors), 2004. pp. 53-60. 2004, Lisbon, Portugal.
ŠAFRÁNEK, David.
Visual Specification of Systems with Heterogeneous Coordination Models. In Proceeding of 3rd International Workshop on Foundations of Coordination Languages and Software Architectures. London : ENTCS, 2004. pp. 107-121. 2004, LondonVol. 180, Issue 2.
KRČÁL, Pavel.
Distributed Explicit Bounded LTL Model Checking. In Second International Workshop on Parallel and Distributed Model Checking. Vyd. 89. Neuveden : Elsevier, 2003. pp. 30-47. 2003, Boulder, Colorado, USA.
ČERNÁ, Ivana - PELÁNEK, Radek.
Distributed Explicit Fair Cycle Detection. In SPIN Workshop 2003. Portland (Oregon, USA) : Springer-Verlag, 2003. ISBN 3-540-40117-2, pp. 49-74. 2003, Portland.
BRIM, Luboš - BARNAT, Jiří.
Distribution of Explicit-State LTL Model-Checking. Electronic Notes in Theoretical Computer Science, , Elsevier Science, The Nederlands. 2003, vol. Volume 80, no. 1, pp. 120-125. Proc. 8th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'03).
PELÁNEK, Radek.
LTL Hierarchies and Model Checking. In Proceedings of the Eight ESSLLI Student Session. Wien : TU Wien, 2003. pp. 245-254. Wien.
ANTOŠ, David - KOŘENEK, Jan - MINAŘÍKOVÁ, Kateřina - ŘEHÁK, Vojtěch.
Packet header matching in Combo6 IPv6 router. CESNET, z.s.p.o., 2003. WWW.
BRIM, Lubos - ČERNÁ, Ivana - HEJTMÁNEK, Lukáš.
Parallel Algorithms for Detection of Negative Cycles. Brno : Faculty of Informatics, 2003. 14 s. Technical Reports, FIMU-RS-2003-04. Full version of the PARCO'03 paper.
BRIM, Lubos - ČERNÁ, Ivana - HEJTMÁNEK, Lukáš.
Parallel Algorithms for Detection of Negative Cycles. In Proceedings of the 10th ParCo Conference. Holandsko : Elsevier B.V., 2003. pp. 98-111. Dresden, Germany.
BARNAT, Jiří - BRIM, Luboš - CHALOUPKA, Jakub.
Parallel Breadth-First Search LTL Model-Checking. In 18th IEEE International Conference on Automated Software Engineering (ASE'03). Montreal : IEEE Computer Society, 2003. ISBN 0-7695-2035-9, pp. 106-115. 2003, Montreal, Canada.
BRIM, Luboš - GRUMBERG, Orna.
PDMC 2003 - Parallel and Distributed Model Checking. Proceedings. Nizozemsko : Elsevier, 2003. 130 s. ENTCS, Vol. 89, No. 1.
ČERNÁ, Ivana - PELÁNEK, Radek.
Relating Hierarchy of Linear Temporal Properties to Model Checking. Brno, Czech Republic : FI MU, 2003. Technical report FIMU-RS-2003-03.
ČERNÁ, Ivana - PELÁNEK, Radek.
Relating Hierarchy of Temporal Properties to Model Checking. In Mathematical Foundations of Computer Science (MFCS 2003). Bratislava (Slovensko) : Springer-Verlag, 2003. ISBN 3-540-40671-9, pp. 318-327. 2003, Bratislava.
BEHRMANN, Gerd - LARSEN, Kim G. - PELÁNEK, Radek.
To Store or Not To Store. In Computer Aided Verification (CAV 2003). Boulder (Colorado, USA) : Springer-Verlag, 2003. ISBN 3-540-40524-0, pp. 433-445. 2003, Boulder.
BRIM, Luboš - ŽÍDKOVÁ, Jitka.
Using Assumptions to Distribute Alternation Free mu-Calculus Model Checking. In 2st International Workshop on Parallel and Distributed Model Checking (PDMC 2003). Vyd. Boulder, Colorado, USA. Brno, Czech Republic : Elsevier, 2003. pp. 19-34. 2003, Boulder, Colorado, USA.
ŽÍDKOVÁ, Jitka.
Using Assumptions to Distribute Model Checking. In Počítačové Architektury & Diagnostika. Brno, Česká republika : Vysoké učení technické v Brně, Fakulta Informačních technologií, Ustav počítačových systémů, 2003. ISBN 80-214-2471-0, pp. 73-78. 24.9.2003, Zvíkovské Podhradí.
KRATOCHVÍLA, Tomáš - ŘEHÁK, Vojtěch - ŠIMEČEK, Pavel.
Verification of COMBO6 VHDL Design. Praha : CESNET, z.s.p.o., 2003. CESNET Technical Report No. 17/2003. WWW.
ANTOŠ, David - KOŘENEK, Jan - ŘEHÁK, Vojtěch.
Vyhledávání v IPv6 směrovači implementovaném v hradlovém poli. In EurOpen, Sborník příspěvků XXIII. konference. Strážnice : EurOpen, 2003. ISBN 80-86583-04-X, pp. 91-102. 29.9.2003, Strážnice.
