appearance

MU › Research and development › List of projects › Project details › Research Project Results

Skip navigation

Skip the Organizational structure panel
Organizational structure
On selecting a constituent part of MU the "Overview of publishing activities" page will be displayed with information relevant to the selected constituent part. The "Overview of publishing activities" page is not available for non-activated items.

Masaryk University
- Faculties
- Law
- Medicine
- Science
- Arts
- Education
- Economics
- Informatics
- Social Studies
- Sports Studies
- Institutes
- Computer Science
- Political Science
- CEITEC
- Specialized Units
- Hostels & Canteens
- University Press
- Telč Centre
- UCB Management
- Rector`s Office
- Rectorate
- Other Units
- Archive
- Language Centre
- International Studies
- Disabled Students
- Technology Transfer
- Biostatistics
- Mendel Museum
- CERIT
- Civic Education

Masaryk University

Research Project Results

<< back

Algorithms and tools for practical verification of concurrent systems.

Project Identification:	GA201/00/1023
MU Investigator:	Prof. RNDr. Luboš Brim, CSc.
MU Faculty/Unit:	Faculty of Informatics
Project Period:	1/2000 - 1/2002
Investor/Programme:	Czech Science Foundation / Standard Projects-

Publications:

2003

Model checking LTL with regular valuations for pushdown systems

ESPARZA, Javier - KUČERA, Antonín - SCHWOON, Stefan.
Model checking LTL with regular valuations for pushdown systems. Information and Computation, , Academic Press, USA. ISSN 0890-5401, 2003, vol. 186, no. 2, pp. 355-376.

2002

$\xor$-OBDD in Symbolic Model Checking

ŘEHÁK, Vojtěch.
$\xor$-OBDD in Symbolic Model Checking. In SOFSEM 2002: Student Research Forum. Milovy (Czech Republic) : Slovak University of Technology, 2002. pp. 41-46. 2002, November 27 2002, Milovy.

Automatizovaná formální verifikace (in Czech)

BRIM, Luboš.
Automatizovaná formální verifikace. In XXI. conference EurOpen 2002. Znojmo, Czech republic. Znojmo, Czech Republic : EuroOpen.cz, Praha, 2002. ISBN 80-86583-00-7, pp. 1-7. 2002, September 30 - October 2, 2002, Znojmo, Czech Re.

CONCUR 2002 - Concurrency Theory. 13th International Conference.

BRIM, Luboš - JANČAR, Petr - KŘETÍNSKÝ, Mojmír - KUČERA, Antonín.
CONCUR 2002 - Concurrency Theory. 13th International Conference. 2002. Czech Republic, Brno. 20.8.2002 - 23.8.2002, Worldwide Activity.

CONCUR 2002 - Concurrency Theory. 13th International Conference. Proceedings.

BRIM, Luboš - JANČAR, Petr - KŘETÍNSKÝ, Mojmír - KUČERA, Antonín.
CONCUR 2002 - Concurrency Theory. 13th International Conference. Proceedings. Berlin, Heidelberg, New York : Springer, 2002. 609 s. Lecture Notes in Computer Science, vol. 2421. ISBN 3-540-44043-7.

Distributed Modular Model Checking

CRHOVÁ, Jitka.
Distributed Modular Model Checking. In 2002 IEEE International Conference on Automated Software Engineering Doctoral Symposium. Edinburgh : 2002. pp. 17-21. 23 - 27 September 2002, Edinburgh, UK.

Distributed Modular Model Checking (abstract)

CRHOVÁ, Jitka.
Distributed Modular Model Checking (abstract). In The Seventeenth IEEE International Conference on Automated Software Engineering. Los Alamitos : IEEE Computer Society, 2002. ISBN 0-7695-1736-6, p. 312-312. 2002, 23 - 27 September 2002, Edinburgh, UK.

Equivalence-Checking with Infinite-State Systems: Techniques and Results.

KUČERA, Antonín - JANČAR, Petr.
Equivalence-Checking with Infinite-State Systems: Techniques and Results. In Proceedings of 29th Conference on Current Trends in Theory and Practice of Informatics (SOFSEM 2002). Berlin : Springer, 2002. ISBN 3-540-00145-X, pp. 41-73. 2002, November 22-29, 2002, Milovy, Czech Republic.

How to distribute LTL model-checking using decomposition of negative claim automaton

BARNAT, Jiří.
How to distribute LTL model-checking using decomposition of negative claim automaton. In SOFSEM 2002 Student Research Forum Proceedings. Milovy,Czech Republic : Slovak University of Technology, 2002. pp. 9-14. 2002, Milovy Czech Republic, November 27, 2002.

Local Distributed Model Checking of RegCTL

ČERNÁ, Ivana - BRÁZDIL, Tomáš.
Local Distributed Model Checking of RegCTL. In PDMC 2002 Parallel and Distributed Model Checking. The Netherlands : Elsevier Science Publishers, 2002. ISBN 0444512918, pp. 1-14. 2002, 19.8.2002, Brno, Czech Republic.

PDMC 2002 - Parallel and Distributed Model Checking.

BRIM, Luboš - GRUMBERG, Orna.
PDMC 2002 - Parallel and Distributed Model Checking. 2002. Kingdom of the Netherlands, Brno. 19.8.2002 - 19.8.2002, Worldwide Activity.

PDMC 2002 - Parallel and Distributed Model Checking. Proceedings.

BRIM, Luboš - GRUMBERG, Orna.
PDMC 2002 - Parallel and Distributed Model Checking. Proceedings. Nizozemsko : Elsevier, 2002. 165 s. ENTCS, Vol. 68, No. 4. ISBN 0444512918.

Property Driven Distribution of Nested DFS

BARNAT, Jiří - BRIM, Luboš - ČERNÁ, Ivana.
Property Driven Distribution of Nested DFS. In M. Leuschel and U. Ultes-Nitsche (Eds.): Proceedings of the 3rd International Workshop on Verification and Computational Logic. Pittsburgh, PA, USA : Dept. of Electronics and Computer Science, University of Southampton, 2002. pp. 1-10. 2002, Pittsburgh, PA, USA, October 2002.

SGCCS: A Graphical Language for Real-Time Coordination

ŠAFRÁNEK, David.
SGCCS: A Graphical Language for Real-Time Coordination. In Proceedings of 1th International Workshop on Foundations of Coordination Languages and Software Architectures. Namur, Belgium : Elsevier Science, 2002. pp. 99-114. 2002, 24.8.2002, Brno, Czech RepublicNutno dodat presna cisla stran.

SGCCS: A Graphical Language for Real-Time Systems

ŠAFRÁNEK, David.
SGCCS: A Graphical Language for Real-Time Systems. In Proceedings SOFSEM 2002 Student Research Forum. Milovy : Mária Bieliková, 2002. pp. 47-52. Best paper award.

The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL

KUČERA, Antonín - STREJČEK, Jan.
The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL. In Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL'02). Berlin : Springer, 2002. ISBN 3-540-44240-5, pp. 276-291. 2002, September 22-25, 2002, Edinburgh, Scotland.

Using Assumptions to Distribute CTL Model Checking

BRIM, Luboš - CRHOVÁ, Jitka - YORAV, Karen.
Using Assumptions to Distribute CTL Model Checking. In 1st International Workshop on Parallel and Distributed Model Checking (PDMC 2002). Brno, Czech Republic : Elsevier, 2002. ISBN 0444512918, pp. 80-95. 2002, August 19, 2002, Brno, Czech republic.

Using Assumptions to Distribute CTL Model Checking

BRIM, Luboš - CRHOVÁ, Jitka - YORAV, Karen.
Using Assumptions to Distribute CTL Model Checking. Brno, Czech Republic : 2002. pp. 1-22. October 2002, Brno, Czech republic.

Using verified property to partition the state space in LTL model-checking

BARNAT, Jiří.
Using verified property to partition the state space in LTL model-checking. In F. Cassez, C. Jard, F. Laroussinie, and M.D. Ryan (Eds.): Modelling and Verification of Parallel processes. Nantes, France : IRCCyN, Ecole Centrale de Nantes, 2002. pp. 262-267. 2002, Nantes, France, June 2002.

YAHODA: verification tools database

CRHOVÁ, Jitka - KRČÁL, Pavel - STREJČEK, Jan - ŠAFRÁNEK, David - ŠIMEČEK, Pavel.
YAHODA: verification tools database. In Proceedings of Tools Day. Brno : FI MU, 2002. pp. 99-103. 2002, 24. 8. 2002, Brno, Czech Republic.

2001

Clinical results of the epithelial flap replacement in photorefractive surgery- 18months follow-up.

AUTRATA, Rudolf - ŘEHŮŘEK, Jaroslav.
Clinical results of the epithelial flap replacement in photorefractive surgery- 18months follow-up. In Book of Abstracts of XIX.Congress of the ESCRS. AMSTERDAM : ECSRS, 2001. ISBN 7856-3412, pp. 221-223. 1.-5.9.2001,Amsterdam.

Distributed LTL Model-Checking Based on Negative Cycle Detection

BRIM, Luboš - ČERNÁ, Ivana - KRČÁL, Pavel - PELÁNEK, Radek.
Distributed LTL Model-Checking Based on Negative Cycle Detection. In FST-TCS 2001. Bangalore, India : Springer, 2001. ISBN 3-540-43002-4, pp. 96-110. Bangalore, India.

Distributed LTL Model-Checking in SPIN

BARNAT, Jiří - BRIM, Luboš - STŘÍBRNÁ, Jitka.
Distributed LTL Model-Checking in SPIN. In M.B. Dwyer (Ed.): Model Checking Software, 8th International SPIN Workshop. Toronto, Canada : Springer Verlag, 2001. ISBN 3-540-42124-6, pp. 200-215. Toronto, Canada, May 2001.

Distributed Shortest Paths for Directed Graphs with Negative Edge Lengths

BRIM, Luboš - ČERNÁ, Ivana - KRČÁL, Pavel - PELÁNEK, Radek.
Distributed Shortest Paths for Directed Graphs with Negative Edge Lengths. Brno : FI MU, 2001. 19 s. Technical Reports, FIMU-RS-2001-01.

How to Employ Reverse Search in Distributed Single-Source Shortest Paths

BRIM, Luboš - ČERNÁ, Ivana - KRČÁL, Pavel - PELÁNEK, Radek.
How to Employ Reverse Search in Distributed Single-Source Shortest Paths. In SOFSEM 2001. Piestany : Springer, 2001. ISBN 3-540-42912-3, pp. 191-200. Piestany, Slovensko.

How to Employ Reverse Search in Distributed Single-Source Shortest Paths

BRIM, Luboš - ČERNÁ, Ivana - KRČÁL, Pavel - PELÁNEK, Radek.
How to Employ Reverse Search in Distributed Single-Source Shortest Paths. Brno : FI MU, 2001. 22 s. Technical Reports, FIMU-RS-2001-09.

Characterizing Non-Zenoness on Real-Time Processes (in Czech)

STŘÍBRNÁ, Jitka - LEE, Insup.
Characterizing Non-Zenoness on Real-Time Processes. BRICS Aalborg : 2nd workshop on Models for Time Critical Systems, Aalborg, Denmark, 2001. 10 s.

Model-Checking LTL with Regular Valuations for Pushdown Systems

ESPARZA, Javier - KUČERA, Antonín - SCHWOON, Stefan.
Model-Checking LTL with Regular Valuations for Pushdown Systems. In Proceedings of 4th International Symposium on Theoretical Aspects of Computer Software (TACS 2001). Berlin, Heidelberg, New York : Springer, 2001. ISBN 3-540-42736-8, pp. 316-340. October 2001, Sendai, Japan.

Randomization Helps in LTL Model Checking

BRIM, Luboš - ČERNÁ, Ivana - NEČESAL, Martin.
Randomization Helps in LTL Model Checking. In Process Algebra and Probabilistic Methods. Proceedings of PAPM-PROBMIV 2001. Berlin Heidelberg New York : Springer, 2001. ISBN 3-540-42556-X, pp. 105-119. Aachen, Germany, September 12-14, 2001.

2000

Constrained Rewrite Transition Systems

STREJČEK, Jan.
Constrained Rewrite Transition Systems. Brno : FI MU, 2000. Report Series, FIMU-RS-2000-12. link to a new window WWW.

Distributed LTL Model-Checking in SPIN (in Czech)

BARNAT, Jiří - BRIM, Luboš - STŘÍBRNÁ, Jitka.
Distributed LTL Model-Checking in SPIN. Brno : FI MU, 2000. 16 s. Technical Reports.

JOMP Application Program Interface

BULL, Mark - OBDRŽÁLEK, Jan.
JOMP Application Program Interface. Vyd. Version 0.1 (draft). Edinburgh : EPCC Technical Report, 2000. 32 s.

On Simulation-Checking with Sequential Systems

KUČERA, Antonín.
On Simulation-Checking with Sequential Systems. In Proceedings of 6th Asian Computing Science Conference (ASIAN 2000). Berlin, Heidelberg, New York : Springer, 2000. ISBN 3-540-41428-2, pp. 133-148. November 2000, Penang, Malaysia.

OpenMP for Java

OBDRŽÁLEK, Jan.
OpenMP for Java. University of Edinburgh : EPCC Technical Report, 2000. 25 s.

Towards OpenMP for Java

BULL, Mark - KAMBITES, Mark - OBDRŽÁLEK, Jan - WESTHEAD, Martin.
Towards OpenMP for Java. In Proceedings of the Second European Workshop on OpenMP (EWOMP 2000). Edinburgh : University of Edinburgh, 2000. pp. 98-105. 2000, University of Edinburgh.

top