Rozvrh

Osnova

• Programy jako transformátory predikátů. Nejslabší vstupní podmínka (wp), vlastnosti transformátorů, správnost algoritmu.
• Programovací jazyk GCL. Syntaxe, definice sémantiky pomocí transformátorů predikátů, SKIP, ABORT, vícenásobné přiřazení, sekvence, alternativa, cyklus.
• Programátorská logika. Zákon sekvence, zákon alternativy, zákon cyklu, vektorové proměnné.
• Návrh algoritmů. Principy a strategie pro návrh založené na programátorské logice, zákon současného návrhu a verifikace.
• Příklady aplikace metodologie na návrh konkrétních algoritmů. Návrh efektivních algoritmů, vyhledávání a třídění.

Požadavky na absolvování předmětu

Předmět je zakončen písemnou zkouškou. Použití literatury a poznámek není při písemce povoleno. Znalosti a dovednosti, které je potřeba zvládnout, jsou uvedeny v katalogu předmětů. Za písemku je možné získat 20 bodů, k absolvování předmětu zkouškou stačí zpravidla polovina. Každá písemka je ovšem jinak obtížná, proto nelze uvést generickou hodnotu. U každé písemky je vždy uveden konkrétní počet bodů pro jednotlivá hodnocení.

Doporučená literatura

• starší text k přednášce (dostupný pouze z domény .muni.cz)

1. Dijkstra, Edsger W. - Feijen, W. H. J. A method of programming. Wokingham : Addison-Wesley Publishing Company, 1998.
2. Kaldewaij, A. (Anne). Programming : the derivation of algorithms. New York : Prentice Hall, 1990.
3. Gries, David. The Science of Programming . New York : Springer-Verlag, 1981.

Doporučené učební pomůcky (PP)

Předmět je pro větší pedagogickou názornost doplněn o výuku pomocí speciální učební pomůcky, kterou je deduktívní hra pro jednoho hráče NSD - najväčší spoločný deliteľ. Tuto hru jsem obdržel jako sponzorský dar od nadnárodního koncernu Martin Ukrop, Ltd.. Jedná se o limitovanou neprodejnou sérii. Tímto bych velice rád poděkoval tvůrcům hry za podnětný a unikátní počin.

Close

Rozvrh

Osnova

Každý program je zpravidla strukturován do několika dílčích menších programů, které realizují část z požadovaných funkcí celého programu. Schopnost vytvářet malé dokonalé programy se proto jeví jako zásadní dovednost každého poctivého programátora. Tento kurz je věnován tomu, jak psát malé a při tom elegantní, ale hlavně správné a efektivní programy. Ukážeme, jak několik jednoduchých postupů a principů může k naplnění tohoto cíle stačit. Jen je třeba se s nimi seznámit a prakticky je zvládnout! Proto je převážná část kurzu zaměřena na řešení, často netradičních a zajímavých, algoritmických úloh pomocí metody elegantního programování.

Požadavky na absolvování předmětu

Předmět je zakončen písemnou zkouškou. Použití literatury a poznámek není při písemce povoleno. Znalosti a dovednosti, které je potřeba zvládnout, jsou uvedeny v katalogu předmětů. Za písemku je možné získat 20 bodů, k absolvování předmětu zkouškou stačí zpravidla polovina. Každá písemka je ovšem jinak obtížná, proto nelze uvést generickou hodnotu. U každé písemky je vždy uveden konkrétní počet bodů pro jednotlivá hodnocení.

Doporučená literatura

• starší text k přednášce (dostupný pouze z domény .muni.cz)

1. Dijkstra, Edsger W. - Feijen, W. H. J. A method of programming. Wokingham : Addison-Wesley Publishing Company, 1998.
2. Kaldewaij, A. (Anne). Programming : the derivation of algorithms. New York : Prentice Hall, 1990.
3. Gries, David. The Science of Programming . New York : Springer-Verlag, 1981.

Doporučené učební pomůcky (PP)

Předmět je pro větší pedagogickou názornost doplněn o výuku pomocí speciální učební pomůcky, kterou je deduktívní hra pro jednoho hráče NSD - najväčší spoločný deliteľ. Tuto hru jsem obdržel jako sponzorský dar od nadnárodního koncernu Martin Ukrop, Ltd.. Jedná se o limitovanou neprodejnou sérii. Tímto bych velice rád poděkoval tvůrcům hry za podnětný a unikátní počin.

Close

Pojem procesu je fundamentálním pojmem informatiky. V oblasti komunikujících systémů hraje stejnou roli jako pojem algoritmu u sekvenčních programů. Cílem předmětu je definovat pojem procesu formálně, získat základní dovednosti, které jsou používány pro formální specifikaci a analýzu komunikujících systémů, včetně teoretických základů příslušných formálních nástrojů. Po absolvování kurzu získají studenti schopnost specifikovat a implementovat v jazyce CCS jednoduché komunikační protokoly; analyzovat a formálně ověřovat korektnost návrhu; orientovat se v nejčastějších typech ekvivalencí mezi procesy a jejich omezení.

Rozvrh

Středa 14.00 - 16.50, B411

Osnova

1. Přehled modelů souběžných systémů. Modelování komunikace. Komunikační media, příklady komunikujících systémů, ekvivalence procesů.
2. Jazyk CCS. Synchronizace, akce a přechody, vnitřní akce, sémantika, synchronizační stromy, předávání hodnot, rekurze a indukce.
3. Rovnostní zákony a jejich aplikace. Klasifikace kombinátorů a zákonů, dynamické zákony, expanzní věta, statické zákony.
4. Bisimulace a ekvivalence. Silná bisimulace a její vlastnosti, silná kongruence, bisimulace a její vlastnosti, dokazování správnosti komunikujícího systému.
5. Teorie kongruence vzhledem k~pozorování. Experiment, rovnosti a jejich vlastnosti, řešení rovností, konečné procesy.
6. Temporální vlastnosti procesů, Hennessy-Milnerova logika, Modální mu kalkul

Požadavky na absolvování předmětu

Předmět je zakončen ústní zkouškou.

Doporučená literatura

1. Milner, Robin. Communication and concurrency. Prentice Hall, 1989.
2. Milner, Robin. Communicating and mobile systems : the Pi calculus. Cambridge University Press, 1999.
3. L. Aceto, A. Ingolfsdottir, K. G. Larsen, J. Srba. Reactive Systems: Modelling, Specification and Verification.. Cambridge University Press, 2007.
4. Učební text k přednáškám. (Materiály jsou dostupné pouze z domény .muni.cz)



5. Učební materiály jsou rovněž dostupné v IS.

Slidy k přednáškám

1. Úvod (PDF)
2. Modelování procesů (PDF)
3. CCS na příkladech (PDF)
4. CCS - syntaxe a sémantika (PDF)
5. Silná bisimulace (PDF)
6. Slabá bisimulace (PDF)
7. Další příklady (PDF)
8. Bisimulační kongruence (PDF)
9. Axiomatizace (PDF)
10. Rozšíření jazyka CCS (PDF)
11. Temporální vlastnosti procesů (PDF)
12. CWB (PDF)

Close

Rozvrh

Úterý, 10:00 - 11:50, on-line

Výuka

Předmět je veden formou výuky, která kombinuje přednášky a samostudium. Přednáška je úvodem do daného tématu (viz níže). Samostudium je věnováno samostatné práci studentů s literaturou s cílem seznámit se s tématem podrobně.

Osnova

• Modální logiky: výroková modální logika, modální mu-kalkulus.
• Temporální logiky: výroková temporální logika, lineární a větvící se čas, temporální operátory.
• Logiky pro systémy reálného času.
• Klasifikace vlastností procesů: lokální, globální vlastnosti, živost, bezpečnost.
• Verifikace temporálních vlastností, ověřování modelu (model checking).
• Automatizovaná verifikace, aplikace.

Požadavky na absolvování předmětu

Znalosti a dovednosti, které je potřeba zvládnout, jsou uvedeny v katalogu předmětů. Předmět je zakončen zkouškou, která je tvořena písemnou a ústní částí. Použití literatury a poznámek není při písemce povoleno. Každá písemka je jinak obtížná, proto nelze uvést generickou hodnotu pro absolvování předmětu či postup k ústní části. Ústní část zkoušky není bodována.

Doporučená literatura

• Handbook of logic in computer science. Vol. 2, Background : computational structures. Edited by S. Abramsky - Dov M. Gabbay - T. S. E. Maibaum. Oxford : Clarendon Press, 1992.
• Clarke, Edmund M. - Grumberg, Orna - Peled, Doron. Model checking. Cambridge : MIT Press, 1999.
• Manna, Zohar - Pnueli, Amir. Temporal verification of reactive systems : safety. New York : Springer, 1995.
• Christel Baier and Joost-Pieter Katoen: Principles of Model Checking. MIT Press, 2008.

Studijní materiály

• Učební text. (Materiály jsou dostupné pouze z domény .muni.cz)

Slidy k přednáškám - témata

Slidy jsou dostupné pouze z domény .muni.cz a nesmí být umístěny na veřejně dostupnou doménu!

1. Why we need non-classical logics? (PDF)
2. Formal models of processes (PDF)
3. Propositional modal logic (PDF)
4. Propositional dynamic logic (PDF)
5. Modal algebras (PDF)
6. Decision procedures for PML (PDF)
7. Between modal and temporal logics (PDF)
8. Propositional temporal logics (PDF)
9. Modal mu-calculus (PDF)
10. Completeness of axiom system for PML (PDF)

Close

Předmět je zaměřen na hlubší studium výsledků teorie vyčíslitelnosti s důrazem na osvojení si používaných důkazových metod a technik. • Po skončení kurzu student porozumí základním výsledkům o vyčíslitelnosti nad nespočetnými množinami; bude schopen zhodnotit další poznatky o klasifikaci problémů, zejména aritmetické hierarchii a relativizované teorii vyčíslitelnosti.

Rozvrh

Úterý 12.00 - 13.50, B410

Osnova

1. Kreativní a produktivní množiny, m-úplné množiny a 1-úplné množiny, efektivně neoddělitelné množiny, jednoduché a imunní množiny.
2. Věta o rekurzi, aplikace v logice.
3. Primitivně rekurzívní, totálně rekurzívní a částečně rekurzívní funkce a predikáty, ekvivalence s třídou vyčíslitelných funkcí.
4. Aritmetické množiny a funkce, Goedelova-Rosserova věta o neúplnosti, druhá Goedelova věta o neúplnosti.
5. Relativizovaná teorie vyčíslitelnosti. Programy s orákulem.
6. Kleeneho hierarchie. T-redukce, aritmetická hierarchie, tt-redukovatelnost.
7. Postův problém.
8. Vyčíslitelnost nespočetných množin. Úplné částečně uspořádané množiny, domény.

Požadavky na absolvování předmětu

Předmět je zakončen ústní zkouškou. Student/ka odpovídá na otázky po krátké přípravě. Cílem zkoušení je rozpoznat rozsah a hloubku získaných znalostí, čemuž odpovídá známka za zkoušku. Studenti, kteří si zvolí ukončení předmětu zápočtem, musí získat alespoň známku E-.

Doporučená literatura

Základním studijním materiálem jsou čerstvě renovovaná skripta o vyčíslitelnosti, která jsou dostupná pouze z domény .muni.cz a nesmí být šířena mimo ni:

Close

2023
149	N. Beneš, L. Brim, S. Pastva, D. Šafránek, E. Šmijáková. Phenotype Control of Partially Specified Boolean Networks. CMSB.
148	L. Brim, S. Pastva, D. Šafránek, E. Šmijáková. Temporary and permanent control of partially specified Boolean networks. Biosystems.
147	N. Beneš, L. Brim, O. Huvar, S. Pastva, D. Šafránek. Boolean Network Sketches: A Unifying Framework for Logical Model Inference. Bioinformatics.
146	M. Troják, D. Šafránek, S. Pastva, L. Brim. Rule-based Modelling of Biological Systems Using Regulated Rewriting. Biosystems.
2022
145	M. Troják, D. Šafránek, B. Brozmann, L. Brim. eBCSgen 2.0: Modelling and Analysis of Regulated Rule-based Systems. CMSB 2022.
144	L. Brim, S. Pastva, D. Šafránek, E. Šmijáková. Temporary and Permanent Control of Partially Specified Boolean Networks. BioSystems.
143	N. Beneš, L. Brim, O. Huvar, S. Pastva, D. Šafránek, E. Šmijáková. AEON.py: Python Library for Attractor Analysis in Asynchronous Boolean Networks. Bioinformatics.
142	N. Beneš, L. Brim, J. Kadlecaj, S. Pastva, D. Šafránek. Exploring Attractor Bifurcations in Boolean Networks. BMC Bioinformatics.
141	N. Beneš, L. Brim, S. Pastva, D. Šafránek. BDD-Based Algorithm for SCC Decomposition of Edge-Coloured Graphs. Logical Methods in Computer Science.
2021
140	N. Beneš, L. Brim, S. Pastva, D. Šafránek. Aeon 2021: Bifurcation Decision Trees in Boolean Networks. CMSB 2021.
139	N. Beneš, L. Brim, S. Pastva, D. Šafránek. Computing Bottom SCCs Symbolically Using Transition Guided Reduction. CAV 2021.
138	L. Brim, S. Pastva, D. Šafránek, E. Šmijáková. Parallel One-Step Control of Parametrised Boolean Networks. Mathematics.
137	N. Beneš, L. Brim, S. Pastva, D. Šafránek. Symbolic Coloured SCC Decomposition. TACAS 2021.
2020
136	M. Troják, D. Šafránek, L. Mertová, L. Brim. Executable Biochemical Space for Specification and Analysis of Biochemical System. Plos ONE.
135	M. Troják, D. Šafránek, L. Mertová, L. Brim. eBCSgen: A Software Tool for Biochemical Space Language. CMSB 2020.
134	E. Šmijáková, S. Pastva, D. Šafránek, L. Brim. Parameter Synthesis for Hybrid Systems from Hybrid CTL Specifications. CMSB 2020.
133	N. Benes, L. Brim, J. Kadlecaj, S. Pastva, D. Safranek. AEON: Attractor Bifurcation Analysis of Parametrised Boolean Networks. CAV 2020.
132	N. Benes, L. Brim, S. Pastva, D. Safranek. Digital bifurcation analysis of internet congestion control protocols. International Journal of Bifurcation and Chaos.
131	M. Troják, D. Safránek, L. Mertová, L. Brim. Parameter Synthesis and Robustness Analysis of Rule-Based Models. NFM 2020.
130	N. Benes, L. Brim, S. Pastva, D. Safranek. Parallel Parameter Synthesis Algorithm for Hybrid CTL. Science of Computer Programming.
2019
129	D. Safránek, M. Troják, V. Bruza, T. Vejpustek, J. Papousek, M. Demko, S. Pastva, A. Pejznoch, L. Brim. Barbaric Robustness Monitoring Revisited for STL* in Parasim. CMSB 2019.
128	N. Benes, L. Brim, S. Pastva, D. Safranek. Accelerating Parameter Synthesis using Semi-Algebraic Constraints. iFM 2019.
127	N. Benes, L. Brim, M. Geletka, S. Pastva, D. Safranek. Formal Analysis of Qualitative Long-Term Behaviour in Parametrised Boolean Networks. ICFEM 2019.
126	N. Benes, L. Brim, S. Pastva, D. Safranek. Digital Bifurcation Analysis of TCP Dynamics. TACAS 2019.
125	N. Benes, L. Brim, J. Drazanova, S. Pastva, D. Safranek. Facetal Abstraction for Non-Linear Dynamical Systems Based on Delta-Decidable SMT. HSCC 2019.
2018
124	N. Benes, L. Brim, S. Pastva, D. Safranek. Model Checking Approach to the Analysis of Biological Systems. Chapter in Automated Reasoning for Systems Biology and Medicine. Springer.
123	M. Troják, D. Šafránek, L. Brim, J. Šalagovič, J. Červený. Executable Biochemical Space for Specification and Analysis of Biochemical Systems. SASB 2018.
122	M. Troják, J. Šalagovič, D. Šafránek, J. Červený, L. Brim, M. Hajnal. Executable Biochemical Space for Specification and Analysis of Biochemical Systems. VEDMP 2018.
121	N. Benes, L. Brim, S. Pastva, D. Safranek, M. Trojak, J. Cerveny, J. Salagovic. Fully Automated Attractor Analysis of Cyanobacteria Models. ICSTCC 2018.
2017
121	M. Ceska, F. Danneberg, N. Paoletti, L. Brim, and M. Kwiatkowska. Precise Parameter Synthesis for Stochastic Biochemical Systems. Acta Informatica.
120	N. Benes, L. Brim, M. Demko, M. Hajnal, S. Pastva and D. Safranek. Discrete Bifurcation Analysis with Pithya. CMSB 2017.
119	J. Barnat, N. Benes, L. Brim, M. Demko, M. Hajnal, S. Pastva and D. Safranek. Detecting Attractors in Biological Models with Uncertain Parameters. CMSB 2017.
118	N. Benes, L. Brim, M. Demko, M. Hajnal, S. Pastva and D. Safranek. PITHYA: High-Performance Parameter Synthesis for Biological Models. ISMB 2017.
117	N. Benes, L. Brim, M. Demko, S. Pastva and D. Safranek. Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-Affine Dynamical Systems. CAV 2017.

2016
116	N. Benes, L. Brim, M. Demko, S. Pastva and D. Safranek. A Model Checking Approach to Discrete Bifurcation Analysis. FM 2016.
115	M. Hajnal, D. Šafránek, M. Demko, S. Pastva, P. Krejčí and L. Brim. Toward Modelling and Analysis of Transient and Sustained Behaviour of Signalling Pathways. HSB 2016.
114	M. Demko, N. Benes, L. Brim, S. Pastva, and D. Safranek. High-Performance Symbolic Parameter Synthesis of Biological Models: A Case Study. CMSB 2016.
113	N. Benes, L. Brim, M. Demko, S. Pastva, and D. Safranek. Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-Affine Systems. ATVA 2016.
112	P. Rockai, J. Barnat and L. Brim. Model Checking C++ Programs with Exceptions. Science of Computer Programming.
111	M. Ceska, F. Danneberg, N. Paoletti, L. Brim, and M. Kwiatkowska. Precise Parameter Synthesis for Stochastic Biochemical Systems. Acta Informatica.
110	M. Ceska, P. Pilar, N. Paoletti, L. Brim, and M. Kwiatkowska. PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems. TACAS 2016.
109	J. Barnat, P. Bauch, N. Benes, L. Brim, J. Beran, T. Kratochvila: Analysing Sanity of Requirements for Avionics Systems. Formal Aspects of Computing.

2015
108	L. Brim, M. Demko, S. Pastva and D. Safranek. High-Performance Discrete Bifurcation Analysis for Piecewise-Affine Dynamical Systems. HSB 2015.
107	T. Ded, D. Safranek, M. Trojak, M. Klement, J. Salagovic and L. Brim. Formal Biochemical Space with Semantics in Kappa and BNGL. SASB 2015.
106	L. Brim, M. Ceska, M. Demko, S. Pastva and D. Safranek. Parameter Synthesis by Parallel Coloured CTL Model Checking. CMSB 2015.
105	L. Brim, M. Demko, S. Pastva and D. Safranek. Coloured Model Checking Approach to Parameter Synthesis for Executable Models in Synthetic Biology. VEMDP 2015.
104	A. Abate, M. Ceska, L. Brim, and M. Kwiatkowska. Adaptive Aggregation of Markov Chains: Quantitative Analysis of Chemical Reaction Networks. CAV 2015.

2014
103	M. Klement et al. E-cyanobacterium.org: A Web-based Platform for Systems Biology of Cyanobacteria. CMSB 2014.
102	P. Rockai, J. Barnat and L. Brim. Model Checking C++ with Exceptions. AVOCS 2014.
101	L. Brim, J. Niznan and D. Safranek. Compact Representation of Photosynthesis Dynamics by Rule-based Models. SASB 2014.
100	M. Ceska, D. Safranek, S. Drazan and L. Brim: Robustness Analysis of Stochastic Biochemical Systems. PLoS ONE. [url]
99	L. Brim, P. Dluhos, D. Safranek, T. Vejpustek. STL*: Extending signal temporal logic with signal-value freezing operator. Information and Computation, 236:52-67 (2014). [url]

2013
98	L. Brim and M. Ceska and S. Drazan and D. Safranek: On Robustness Analysis of Stochastic Biochemical Systems by Probabilistic Model Checking. CoRR, volume abs/1310.4734
97	L. Brim, J. Fabrikova, T. Vejpustek and D. Safranek. Robustness Analysis for Value-Freezing Signal Temporal Logic. HSB 2013.
96	S. Van Goethem, J-M. Jacquet, L. Brim, D. Safranek. Timed Modelling of Gene Networks with Arbitrarily Precise Expression Discretization. ENTCS 293:67-81.
95	L. Brim, M. Ceska, S. Drazan and D. Safranek. Robustness Analysis of Stochastic Systems. CompMod 2013.
94	L. Brim, V. Ded and D. Safranek. Qualitative modelling and analysis of Photosystem II. BioPPN 2013.
93	L. Brim, M. Ceska and D. Safranek. Model Checking of Biological Systems. SFM on Design of Computer, Communication and Software Systems: Dynamical Systems. [ url]
92	J. Barnat, L. Brim and V. Havel. LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model. ACSD 2013.[url]
91	L. Brim, M. Ceska, S. Drazan and D. Šafránek. Exploring Parameter Space of Stochastic Biochemical Systems using Quantitative Model Checking. CAV 2013.[url]
90	J. Barnat, L. Brim, V. Havel, J. Havlíček, J. Kriho, M. Lenco, P. Ročkai, V. Štill and J. Weiser. DiVinE 3.0 — Explicit-state Model-checker for Multithreaded C/C++ Programs. CAV 2013.[
89	P. Rockai, J. Barnat and L. Brim. Improved State Space Reductions for LTL Model Checking of C & C++ Programs. NFM 2013.

2012
88	D. Safranek, J. Cerveny, M. Klement, L. Brim, D. Lazar and L. Nedbal: E-photosynthesis: Web-based platform for photosynthetic processes (poster). CMSB'12.
87	L. Brim and J. Chaloupka. Using Strategy Improvement to Stay Alive. Int. J. Found. Comput. Sci.
86	J. Barnat, P. Bauch, L. Brim, and M. Ceska. Designing Fast LTL Model Checking Algorithms for Many-Core GPUs. Journal of Parallel and Distributed Computing. [ url]
85	P. Dluhos, D. Safranek, and L. Brim. On Expressing and Monitoring Oscillatory Dynamics. HSB 2012.
84	L. Brim J. Fabrikova, S. Drazan and D. Safranek. On Approximative Reachability Analysis of Biochemical Dynamical Systems. Transactions on Computational Systems Biology.
83	J. Barnat, P. Bauch, and L. Brim. Checking Sanity of Software Requirements. SEFM 2012.
82	J. Barnat, L. Brim, P. Rockai, J. Beran, and T. Kratochvila. Tool Chain to support Automated Formal Verification of Avionics Simulink Designs. FMICS 2012.
81	S. Van Goethem, J-M. Jacquet, L. Brim and D. Safránek. Timed Modelling of Gene Networks with Arbitrary Expression Level Discretization. CS2Bio12.
80	J. Barnat, L. Brim, J. Beran, T. Kratochvila and R. Oliveira. Executing Model Checking Counterexamples in Simulink. TASE 2012.
79	J. Barnat, L. Brim, A. Krejci, A. Streck, D. Safránek, M. Vejnar, T. Vejpustek: On Parameter Synthesis by Parallel Model Checking. IEEE/ACM Trans. Comput. Biology Bioinform. [ url].
78	J. Barnat, L. Brim and P. Rockai. Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs. NFM 2012.
77	J. Barnat, L. Brim, and P. Rockai:: On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties. Sci. Comput. Program. 77(12). [ url]

2011
76	L. Brim and J. Barnat. Platform Dependent Verification: Engineering Verification Tools for 21st Century . PDMC 2011.
75	L. Brim, J. Fabrikova, S. Drazan and D. Safranek. Reachability in Biochemical Dynamical Systems by Quantitative Discrete Approximation. COMPMOD 2011.
74	J. Barnat, P. Bauch, L. Brim, and M. Ceska. Computing Optimal Cycle Mean in Parallel on CUDA. PDMC 2011.
73	L. Brim, J. Chaloupka, L. Doyen, R. Gentilini and J. F. Raskin: Faster algorithms for mean-payoff games. Formal Methods in System Design 38(2), 2011.
72	D. Safranek, J. Cerveny, M. Klement, J. Pospisilova, L. Brim, D. Lazar and L. Nedbal: E-photosynthesis: Web-based platform for modeling of complex photosynthetic processes. Biosystems 103(2), 2011.
71	J. Barnat, P. Bauch, L. Brim, and M. Ceska. Computing Strongly Connected Components in Parallel on CUDA. IPDPS 2011.
70	S. Edelkamp, D. Sulewski, J. Barnat, L. Brim, and P. Simecek: Flash memory efficient LTL model checking. Sci. Comput. Program. 76(2).

2010
69	J. Barnat, P. Bauch, L. Brim, and M. Ceska. Employing Multiple CUDA Devices to Accelerate LTL Model Checking. ICPADS 2010.
68	J. Barnat, L. Brim, D. Safranek, and M. Vejnar. Parameter Scanning by Parallel Model Checking with Applications to Systems and Synthetic Biology. HiBi 2010.
67	J. Barnat, L. Brim, M. Ceska, and P. Rockai. DiVinE: Parallel Distributed Model Checker. PDMC 2010.
66	L. Brim and J. Chaloupka. Using Strategy Improvement to Stay Alive. Gandalf 2010.
65	J. Barnat, L. Brim, P. Rockai: Parallel Partial Order Reduction with Topological Sort Proviso. SEFM 2010.
64	J. Barnat, L. Brim, P. Rockai: Scalable Multi-Core LTL Model-Checking. STTT.
63	J. Barnat, L. Brim and D. Safranek. High-Performance Analysis of Biological Systems Dynamics with DiVinE. Briefings in Bioinformatics, vol. 11(3).

2009
62	J. Barnat, L. Brim, I. Cerna, S. Drazan, J. Fabrikova and D. Safranek: On algorithmic analysis of transcriptional regulation by LTL model checking. Theor. Comput. Sci., vol. 410(33-34).
61	J. Chaloupka and L. Brim. Faster Algorithm for Mean-Payoff Games. MEMICS 2009.
60	J. Barnat, L. Brim, I. Cerna, S. Drazan, J. Fabrikova and D. Safranek. Computational Analysis of Large-Scale Multi-Affine ODE Models. HiBi 2009.
59	J. Barnat, L. Brim, M. Ceska: DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking. PDMC 2009.
58	J. Barnat, L. Brim, I. Cerna, S. Drazan, J. Fabrikova , J. Lanik and D. Safranek: BioDiVinE: A Tool for Parallel Analysis of Multi-Affine ODE Models. CMSB'09.
57	J. Barnat, L. Brim, I. Cerna, S. Drazan, J. Fabrikova, D. Safranek: BioDiVinE: A Framework for Parallel Analysis of Biological Models. COMPMOD 2009.
56	J. Barnat, L. Brim, M. Ceska, and T. Lamr: CUDA accelerated LTL Model Checking. ICPADS 2009.
55	J. Barnat, L. Brim, and P. Rockai: A Time-Optimal On-the-fly Parallel Algorithm for Model Checking of Weak LTL Properties. ICFEM 2009.
54	J. Barnat, L. Brim, and P. Rockai: DiVinE 2.0: High-Performance Model Checking. HiBi 2009.
53	J. Barnat, L. Brim, and P. Simecek: Cluster-Based I/O-Efficient LTL Model Checking. ASE 2009.
52	J. Barnat, L. Brim, and P. Simecek: Parallel I/O-Efficient State Space Generation. MASSIVE 2009.
51	H. Bal, J. Barnat, L. Brim, and K. Verstoep: Efficient Large-Scale Model Checking. IPDPS 2009.
50	N. Benes, L. Brim, I. Cerna, J. Sochor, P. Varekova and B. Zimmerova: Partial Order Reduction for State/Event LTL. IFM 2009.

2008
49	J. Barnat, L. Brim, I. Cerna, M. Ceska and J. Tumova: Local Quantitative LTL Model Checking. FMICS 2008.
48	J. Barnat, L. Brim, S. Edelkamp, D. Sulewski and P. Simecek: Can Flash Memory Help in Model Checking. FMICS 2008.
47	L. Brim, J. Barnat: Squeeze All the Power Out of Your Hardware to Verify Your Software! ISOLA 2008.
46	J. Barnat, L. Brim, P. Rockai: DiVinE Multi-Core -- A Parallel LTL Model-Checker. ATVA 2008.
45	J. Barnat, L. Brim, I. Cerna, M. Ceska, J. Tumova: ProbDiVinE-MC: Multi-Core LTL Model Checker for Probabilistic Systems. QEST 2008.
44	J. Barnat, L. Brim, P. Simecek, M. Weber: Revisiting Resistance Speeds Up LTL Model Checking. TACAS 2008.

2007
43	J. Barnat, L. Brim, I. Cerna, S. Drazan, D. Safranek: Parallel Model Checking Large-Scale Genetic Regulatory Network with DIVINE. FBTC 2007.
42	J. Barnat, L. Brim, I. Cerna, M. Ceska, J. Tumova: ProbDiVinE - A Parallel Qualitative LTL Model-Checker. QEST 2007.
41	L. Brim, J. Barnat: Tutorial on Parallel Model-Checking. SPIN 2007.
40	J. Barnat, L. Brim, P. Rockai: Scalable Multi-Core LTL Model-Checking. SPIN 2007.
39	J. Barnat, L. Brim, M. Leucker: Parallel Model Checking and the FMICS-jETI Platform. ICECCS 2007.
38	J. Barnat, L. Brim, P. Simecek: I/O Efficient Accepting Cycle Detection. CAV 2007.
37	L. Brim, M. Kretinsky: Model Checking Large Finite-State Systems and Beyond. SOFSEM 2007.

2006
36	J. Barnat, L. Brim, I. Cerna, M. Ceska, J. Tumova: Distributed Qualitative LTL Model Checking of Markov Decision Processes. PDMC 2006.
35	L. Brim, I. Cerna, P. Moravec, J. Simsa: On Combining Partial Order Reduction with Fairness Assumptions. FMICS 2006.
34	L. Brim: Distributed Verification: Exploring the Power of Raw Computing Power. PDMC 2006.
33	J. Barnat, L. Brim, I. Cerna, P. Moravec, P. Rockai, P. Simecek: DiVinE - The Distributed Verification Environment. CAV 2006.
32	Lubos Brim, Ivana Cerna, Pavel Moravec, Jiri Simsa: How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors. Electr. Notes Theor. Comput. Sci. 135 (2): 3-18 (2006)

2005
31	Jiri Barnat, Lubos Brim, Ivana Cerna: Distributed Analysis of Large Systems. FMCO 2005.
30	Barbora Zimmerova, Lubos Brim, Ivana Cerna, Pavlina Varekova: Component-Interaction Automata as a Verification-Oriented Component-Based System Specification. SAVCBS 2005.
29	Radek Pelanek, Tomas Hanzl, Ivana Cerna, Lubos Brim: Enhancing Random Walk State Space Exploration. FMICS 2005.
28	Jiri Barnat, Lubos Brim, Ivana Cerna, Pavel Simecek: DiVinE - The Distributed Verification Environment. PDMC 2005.
27	Lubos Brim, Ivana Cerna, Pavel Moravec, Jiri Simsa: How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors. PDMC 2005.
26	Jiri Barnat, Lubos Brim and Jakub Chaloupka: From Distributed Memory Cycle Detection to Parallel LTL Model Checking. ENTCS 133(1): (2005)
25	Lubos Brim, Ivana Cerna, Pavel Moravec, Jiri Simsa: Distributed Partial Order Reduction of State Spaces. ENTCS 128(3): (2005)
24	Lubos Brim, Orna Grumberg: Introductory Paper: Parallel and Distributed Model-Checking. International Journal on Software Tools for Technology Transfer, Feb. 2005
23	Lubos Brim, Karen Yorav, Jitka Zidkova: Assumption-based distribution of CTL model checking. International Journal on Software Tools for Technology Transfer, Feb. 2005

2004
22	Lubos Brim, Ivana Cerna, Lukas Hejtmanek: Distributed Negative Cycle Detection Algorithms. In Parallel Computing: Software Technology, Algorithms, Architectures & Applications. Elsevier B.V., 2004.
21	Jiri Barnat, Lubos Brim, Jakub Chaloupka: From Distributed Memory Cycle Detection to Parallel LTL Model Checking. FMICS 2004.
20	Lubos Brim, Ivana Cerna, Pavel Moravec, Jiri Simsa: Distributed Partial Order Reduction of State Spaces. PDMC 2004.
19	Lubos Brim, Ivana Cerna, Pavel Moravec, Jiri Simsa: Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking. FMCAD 2004.
18	Lubos Brim: Parallel Model-Checking. ERCIM News, number 58, July 2004.

2003
17	Jiri Barnat, Lubos Brim, Jakub Chaloupka: Parallel Breadth-First Search LTL Model-Checking. ASE 2003.
16	Lubos Brim, Orna Grumberg: Preface. ENTCS 89(1): (2003)
15	Lubos Brim, Jitka Zidkova: Using Assumptions to Distribute Alternation Free Mu-Calculus Model Checking. PDMC 2003 (ENTCS 89.1).
14	Lubos Brim, Ivana Cerna, Lukas Hejtmanek: Distributed Negative Cycle Detection Algorithms. PARCO 2003.
13	Lubos Brim, Mojmír Kretínský, Jean-Marie Jacquet, David Gilbert: Modelling Multi-Agent Systems as Synchronous Concurrent Constraint Processes. Computing and Informatics, Vol. 21, 2002.
12	Lubos Brim, Jiri Barnat: Distribution of Explicit-State LTL Model-Checking. FMICS 2003 (ENTCS 80).
11	Jean-Marie Jacquet, Lubos Brim, David Gilbert, Mojmír Kretínský: Coordination by Means of Synchronous and Asynchronous Communication in Concurrent Constraint Programming. ENTCS 68(3): (2003)

2002
10	Lubos Brim: Automated Formal Verification. EurOpen 2002.
9	Jiri Barnat, Lubos Brim, Ivana Cerna: Property Driven Distribution of Nested DFS. VCL'02.
8	Lubos Brim, Petr Jancar, Mojmír Kretínský, Antonín Kucera: CONCUR 2002 - Concurrency Theory, 13th International Conference, Brno, Czech Republic, August 20-23, 2002, Proceedings. Springer 2002
7	Lubos Brim, Orna Grumberg: Preface. ENTCS 68(4): (2002)
6	Lubos Brim, Jitka Crhova, Karen Yorav: Using Assumptions to Distribute CTL Model Checking. ENTCS 68(4): (2002)

2001
5	Lubos Brim, Ivana Cerna, Pavel Krcál, Radek Pelánek: Distributed LTL Model Checking Based on Negative Cycle Detection. FSTTCS 2001: 96-107
4	Lubos Brim, Ivana Cerna, Martin Necesal: Randomization Helps in LTL Model Checking. PAPM-PROBMIV 2001: 105-119
3	Lubos Brim, Ivana Cerna, Pavel Krcál, Radek Pelánek: How to Employ Reverse Search in Distributed Single Source Shortest Paths. SOFSEM 2001: 191-200
2	Lubos Brim, David Gilbert, Jean-Marie Jacquet, Mojmír Kretínský: Multi-agent Systems as Concurrent Constraint Processes. SOFSEM 2001: 201-210
1	Jiri Barnat, Lubos Brim, Jitka Stríbrná: Distributed LTL Model-Checking in SPIN. SPIN 2001: 200-216

Close