Výsledky výzkumného projektu

<< zpět
 

Verifikace a analýza velmi velkých počítačových systémů

Kód projektu:GA201/09/1389
Řešitel na MU:prof. RNDr. Luboš Brim, CSc.
Fakulta/Pracoviště MU:Fakulta informatiky
Období řešení:1/2009 - 12/2011
Investor/program:Grantová agentura ČR / Standardní projekty-

Publikace:

2012
Almost linear Büchi automata (anglicky)

BABIAK, Tomáš - STREJČEK, Jan - ŘEHÁK, Vojtěch.
Almost linear Büchi automata. Mathematical Structures in Computer Science, Cambridge, Cambridge University Press, Spojené království. ISSN 0960-1295, 2012, vol. 22, no. 2, s. 203-235.

více

 
Designing Fast LTL Model Checking Algorithms for Many-core GPUs (anglicky)

BARNAT, Jiří - BAUCH, Petr - BRIM, Luboš - ČEŠKA, Milan.
Designing Fast LTL Model Checking Algorithms for Many-core GPUs. Journal of Parallel and Distributed Computing, , Elsevier. ISSN 0743-7315, 2012, vol. 72, no. 9, s. 1083-1097.

více

 
LTL to Büchi Automata Translation: Fast and More Deterministic (anglicky)

BABIAK, Tomáš - KŘETÍNSKÝ, Mojmír - ŘEHÁK, Vojtěch - STREJČEK, Jan.
LTL to Büchi Automata Translation: Fast and More Deterministic. In TACAS 2012: 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg : Springer-Verlag, 2012. ISBN 978-3-642-28755-8, s. 95-109. 2012, Tallinn, Estonia.

více

 
On Parameter Synthesis by Parallel Model Checking (anglicky)

BARNAT, Jiří - BRIM, Luboš - KREJČÍ, Adam - STRECK, Adam - ŠAFRÁNEK, David - VEJNÁR, Martin - VEJPUSTEK, Tomáš.
On Parameter Synthesis by Parallel Model Checking. IEEE/ACM Transactions on Computational Biology and Bioinformatics, Los Alamitos, IEEE Computer Society. ISSN 1545-5963, 2012, vol. 9, no. 3, s. 693-705.

více

 
On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties (anglicky)

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, Spojené státy. ISSN 0167-6423, 2012, vol. 77, no. 12, s. 1272-1288.

více

 
Using strategy improvement to stay alive (anglicky)

BRIM, Luboš - CHALOUPKA, Jakub.
Using strategy improvement to stay alive. International Journal of Foundations of Computer Science, , , Spojené království. ISSN 0129-0541, 2012, vol. 23, no. 3, s. 585-608.

více

 
2011
CoInDiVinE: Parallel Distributed Model Checker for Component-Based Systems (anglicky)

BENEŠ, Nikola - ČERNÁ, Ivana - KŘIVÁNEK, Milan.
CoInDiVinE: Parallel Distributed Model Checker for Component-Based Systems. In Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation. Neuveden : Open Publishing Association, 2011. s. 63-67. 2011, Snowbird, Utah, USA.

více

 
Computing Optimal Cycle Mean in Parallel on CUDA (anglicky)

BARNAT, Jiří - BAUCH, Petr - BRIM, Luboš - ČEŠKA, Milan.
Computing Optimal Cycle Mean in Parallel on CUDA. Electronic Proceedings in Theoretical Computer Science, , , Spojené státy. ISSN 2075-2180, 2011, vol. 72, no. 2011, s. 68-83. PDMC 2011.

více

 
Computing Strongly Connected Components in Parallel on CUDA (anglicky)

BARNAT, Jiří - BAUCH, Petr - BRIM, Luboš - ČEŠKA, Milan.
Computing Strongly Connected Components in Parallel on CUDA. In Proceedings of 25th IEEE International Parallel & Distributed Processing Symposium. Anchorage, AK : IEEE Computer Society, 2011. ISBN 978-1-61284-372-8, s. 544 - 555.

více

 
CUDA Accelerated LTL Model Checking - Revisited (anglicky)

BAUCH, Petr - ČEŠKA, Milan.
CUDA Accelerated LTL Model Checking - Revisited. In Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers. Dagstuhl, Germany : Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2011. ISBN 978-3-939897-22-4, s. 1--8.

více

 
Distributed Algorithms for SCC Decomposition (anglicky)

BARNAT, Jiří - CHALOUPKA, Jakub - VAN DE POL, Jaco.
Distributed Algorithms for SCC Decomposition. Journal of Logic and Computation, , Oxford University Press, Spojené království. ISSN 0955-792X, 2011, vol. 21, no. 1, s. 23-44.

více

 
E-photosynthesis: Web-based platform for modeling of complex photosynthetic processes (anglicky)

ŠAFRÁNEK, David - ČERVENÝ, Jan - KLEMENT, Matej - POSPÍŠILOVÁ, Jana - BRIM, Luboš - LAZÁR, Dušan - NEDBAL, Ladislav.
E-photosynthesis: Web-based platform for modeling of complex photosynthetic processes. BioSystems, , Elsevier. ISSN 0303-2647, 2011, vol. 103, no. 2, s. 115-124.

více

 
Faster algorithms for mean-payoff games (anglicky)

BRIM, Luboš - CHALOUPKA, Jakub - DOYEN, Laurent - GENTILINI, Raffaella - RASKIN, Jean-François.
Faster algorithms for mean-payoff games. Formal Methods in System Design, , Springer Netherlands, Nizozemsko. ISSN 0925-9856, 2011, vol. 38, no. 2, s. 97-118.

více

 
Partial Order Reduction for State/Event LTL with Application to Component-Interaction Automata (anglicky)

BENEŠ, Nikola - BRIM, Luboš - BÜHNOVÁ, Barbora - ČERNÁ, Ivana - SOCHOR, Jiří - MORAVCOVÁ VAŘEKOVÁ, Pavlína.
Partial Order Reduction for State/Event LTL with Application to Component-Interaction Automata. Science of Computer Programming, , Elsevier, Spojené státy. ISSN 0167-6423, 2011, vol. 76, no. 10, s. 877-890.

více

 
Reachability in Biochemical Dynamical Systems by Quantitative Discrete Approximation (anglicky)

BRIM, Luboš - FABRIKOVÁ, Jana - DRAŽAN, Sven - ŠAFRÁNEK, David.
Reachability in Biochemical Dynamical Systems by Quantitative Discrete Approximation. Electronic Proceedings in Theoretical Computer Science, , , Spojené státy. ISSN 2075-2180, 2011, vol. Neuveden, no. 67, s. 97-112.

více

 
2010
A Symbolic Approach to Controlling Piecewise Affine Systems (anglicky)

TŮMOVÁ, Jana - YORDANOV, Boyan - BELTA, Calin - ČERNÁ, Ivana - BARNAT, Jiří.
A Symbolic Approach to Controlling Piecewise Affine Systems. In Proceedings of of the 49th IEEE Conference on Decision and Control (CDC). Neuveden : Omnipress for IEEE Control Systems Society, 2010. ISBN 978-1-4244-7744-9, s. 4230-4235. 2010, Atlanta, GA, USA.

více

 
Algorithm for Two-Energy Games (anglicky)

CHALOUPKA, Jakub.
Algorithm for Two-Energy Games. In Mathematical and Engineering Methods in Computer Science (MEMICS) 2010. Brno : NOVPRESS s.r.o., 2010. ISBN 978-80-87342-10-7, 9 s. Mikulov.

více

 
Almost Linear Büchi Automata (anglicky)

BABIAK, Tomáš - STREJČEK, Jan - ŘEHÁK, Vojtěch.
Almost Linear Büchi Automata. 2010.

více

 
CoIn-DiVinE (anglicky)

BENEŠ, Nikola - ČERNÁ, Ivana - KŘIVÁNEK, Milan.
CoIn-DiVinE. 2010.

více

 
CUDA Accelerated LTL Model Checking -- Revisited 

BAUCH, Petr - ČEŠKA, Milan.
CUDA Accelerated LTL Model Checking -- Revisited. In Proceedings of 6th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2010). Brno : NOVPRESS, 2010. ISBN 978-80-87342-10-7, s. 11-19. 2010, Mikulov, Česká republika.

více

 
DiVinE 2.4 

BARNAT, Jiří - BRIM, Luboš - ROČKAI, Petr.
DiVinE 2.4. 2010.

více

 
DiVinE: Parallel Distributed Model Checker (Tool paper) 

BARNAT, Jiří - BRIM, Luboš - ČEŠKA, Milan - ROČKAI, Petr.
DiVinE: Parallel Distributed Model Checker (Tool paper). In Proceedings of joint HiBi/PDMC workshop (HiBi/PDMC 2010). : 2010. 4 s. 2010, Twente, Netherlands.

více

 
Employing Multiple CUDA Devices to Accelerate LTL Model Checking (anglicky)

BARNAT, Jiří - BAUCH, Petr - BRIM, Luboš - ČEŠKA, Milan.
Employing Multiple CUDA Devices to Accelerate LTL Model Checking. In Proceedings of 16th International Conference on Parallel and Distributed Systems (ICPADS 2010). Neuveden : IEEE Computer Society, 2010. ISBN 978-0-7695-4307-9, s. 259-266. 2010, Shanghai, China.

více

 
E-photosynthesis: web software for modeling and analysis of biological processes behind photosynthesis (anglicky)

KLEMENT, Matej - ŠAFRÁNEK, David - ČERVENÝ, Jan - BRIM, Luboš - NEDBAL, Ladislav.
E-photosynthesis: web software for modeling and analysis of biological processes behind photosynthesis. 2010.

více

 
Formal Analysis of Piecewise Affine Systems through Formula-Guided Refinement (anglicky)

YORDANOV, Boyan - TŮMOVÁ, Jana - BELTA, Calin - ČERNÁ, Ivana - BARNAT, Jiří.
Formal Analysis of Piecewise Affine Systems through Formula-Guided Refinement. In Proceedings of of the 49th IEEE Conference on Decision and Control (CDC). Neuveden : Omnipress for IEEE Control Systems Society, 2010. ISBN 978-1-4244-7744-9, s. 5899-5904. 2010, Atlanta, GA, USA.

více

 
Formal Verification of Component-based Architectures - Motivation, Methods & Challenges (anglicky)

ČERNÁ, Ivana.
Formal Verification of Component-based Architectures - Motivation, Methods & Challenges. 2010.

více

 
High-performance analysis of biological systems dynamics with the DiVinE model checker (anglicky)

BARNAT, Jiří - BRIM, Luboš - ŠAFRÁNEK, David.
High-performance analysis of biological systems dynamics with the DiVinE model checker. Briefings in Bioinformatics, Oxford (UK), Oxford University Press. ISSN 1467-5463, 2010, vol. 11, no. 3, s. 301-312.

více

 
MWC-DiVinE (anglicky)

BARNAT, Jiří - BRIM, Luboš - BAUCH, Petr - ČEŠKA, Milan.
MWC-DiVinE. 2010.

více

 
Optimal Path Planning under Temporal Logic Contstraints (anglicky)

SMITH, Stephen L. - TŮMOVÁ, Jana - BELTA, Calin - RUS, Daniela.
Optimal Path Planning under Temporal Logic Contstraints. In Proceedings of the 2010 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS 2010). Neuveden : IEEE, 2010. ISBN 978-1-4244-6675-7, s. 3288-3293. 2010, Taipei, Taiwan.

více

 
Parallel Partial Order Reduction with Topological Sort Proviso (anglicky)

BARNAT, Jiří - BRIM, Luboš - ROČKAI, Petr.
Parallel Partial Order Reduction with Topological Sort Proviso. In Software Engineering and Formal Methods (SEFM 2010). Los Alamos : IEEE Computer Society Press, 2010. ISBN 978-0-7695-4153-2, s. 222-231. 2010, CNR, Pisa, Italy.

více

 
Parameter Scanning by Parallel Model Checking with Applications in Systems Biology (anglicky)

BARNAT, Jiří - BRIM, Luboš - ŠAFRÁNEK, David - VEJNÁR, Martin.
Parameter Scanning by Parallel Model Checking with Applications in Systems Biology. In Ninth International Workshop on Parallel and Distributed Methods in Verification, and Second International Workshop on High Performance Computational Systems Biology. Los Alamitos : IEEE Computer Society, 2010. ISBN 978-0-7695-4265-2, s. 95-104. 2010, Enschede.

více

 
ProbDiVinE 2.0 (anglicky)

APPL, Jiří - BARNAT, Jiří - BRIM, Luboš - ČERNÁ, Ivana - ČEŠKA, Milan - TŮMOVÁ, Jana.
ProbDiVinE 2.0. 2010.

více

 
Scalable shared memory LTL model checking (anglicky)

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, Německo. ISSN 1433-2779, 2010, vol. 12, no. 2, s. 139-153.

více

 
Translation of LTL to Büchi Automata: Improved Once Again (anglicky)

BABIAK, Tomáš.
Translation of LTL to Büchi Automata: Improved Once Again. In Proceedings of 9th International Summer School on Modelling and Verifying Parallel Processes 2010 (MOVEP 2010). Aachen, Germany : 2010. s. 41-46. 28.6.2010, Aachen, Germany.

více

 
Using Strategy Improvement to Stay Alive (anglicky)

BRIM, Luboš - CHALOUPKA, Jakub.
Using Strategy Improvement to Stay Alive. In Games, Automata, Logics and Formal Verification (GandALF) 2010. Neuveden : Electronic Proceedings in Theoretical Computer Science (EPTCS), 2010. s. 40-54. 2010, Minori, Itálie.

více

 
Z-reachability Problem for Games on 2-dimensional Vector Addition Systems with States is in P (anglicky)

CHALOUPKA, Jakub.
Z-reachability Problem for Games on 2-dimensional Vector Addition Systems with States is in P. In Reachability Problems. Berlin : Springer Berlin / Heidelberg, 2010. ISBN 978-3-642-15348-8, s. 104-119. 2010, Brno.

více

 
2009
A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties (anglicky)

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, s. 407-425. 2009, Rio de Janeiro.

více

 
BioDiVinE (anglicky)

BARNAT, Jiří - DRAŽAN, Sven - FABRIKOVÁ, Jana - ŠAFRÁNEK, David - BRIM, Luboš - ČERNÁ, Ivana - LÁNÍK, Jan.
BioDiVinE. 2009.

více

 
BioDiVinE: A Framework for Parallel Analysis of Biological Models (anglicky)

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. s. 31-45. 2009, Eindhoven.

více

 
BIOMS: Biological Models Specification Tool (anglicky)

BRIM, Luboš - ŠAFRÁNEK, David - VRBAS, Jakub.
BIOMS: Biological Models Specification Tool. 2009.

více

 
Cluster-Based I/O-Efficient LTL Model Checking (anglicky)

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, s. 635-639. 2009, Auckalnd, New Zealand.

více

 
CoIn Tool Set (anglicky)

BENEŠ, Nikola - BÜHNOVÁ, Barbora - ČERNÁ, Ivana - KŘIVÁNEK, Milan.
CoIn Tool Set. 2009.

více

 
CUDA Accelerated LTL Model Checking (anglicky)

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, s. 34-41. 8.12.2009, Shezhen, Čína.

více

 
DiVinE 2.0 (anglicky)

ROČKAI, Petr - BARNAT, Jiří - BRIM, Luboš - ČEŠKA, Milan.
DiVinE 2.0. 2009.

více

 
DiVinE 2.0: High-Performance Model Checking (anglicky)

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, s. 31-32. 2009, Trento.

více

 
DiVinE Cuda (anglicky)

BARNAT, Jiří - BRIM, Luboš - BAUCH, Petr - ČEŠKA, Milan - LAMR, Tomáš.
DiVinE Cuda. 2009.

více

 
Efficient Large-Scale Model Checking (anglicky)

VERSTOEP, Kees - BAL, Henri E. - BARNAT, Jiří - BRIM, Luboš.
Efficient Large-Scale Model Checking. In 23rd IEEE International Parallel & Distributed Processing Symposium. IEEE : IEEE, 2009. ISBN 978-1-4244-3751-1, s. 201-212. 2009, Rome, Italy.

více

 
Faster Algorithm for Mean-Payoff Games (anglicky)

CHALOUPKA, Jakub - BRIM, Luboš.
Faster Algorithm for Mean-Payoff Games. In MEMICS 2009. Brno : NOVPRESS s.r.o., 2009. ISBN 978-80-87342-04-6, s. 45-53. Znojmo.

více

 
Faster Algorithm for Mean-Payoff Games (anglicky)

CHALOUPKA, Jakub - BRIM, Luboš.
Faster Algorithm for Mean-Payoff Games. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Dagstuhl, Německo : Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Německo, 2009. ISBN 978-3-939897-15-6, 9 s. Znojmo, Česká republika.

více

 
On Algorithmic Analysis of Transcriptional Regulation by LTL Model Checking (anglicky)

BARNAT, Jiří - BRIM, Luboš - ČERNÁ, Ivana - DRAŽAN, Sven - FABRIKOVÁ, Jana - ŠAFRÁNEK, David.
On Algorithmic Analysis of Transcriptional Regulation by LTL Model Checking. Theoretical Computer Science. ISSN 0304-3975, 2009, vol. 2009, no. 410, s. 3128-3148.

více

 
On Decidability of LTL+Past Model Checking for Process Rewrite Systems (anglicky)

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. s. 105-117. 2007, Lisbon, Portugal.

více

 
On Determinism in Modal Transition Systems (anglicky)

BENEŠ, Nikola - KŘETÍNSKÝ, Jan - LARSEN, Kim G. - SRBA, Jiří.
On Determinism in Modal Transition Systems. Theoretical Computer Science, , Elsevier, Nizozemsko. ISSN 0304-3975, 2009, vol. 410/2009, no. 41, s. 4026-4043.

více

 
Parallel Algorithms for Mean-Payoff Games: An Experimental Evaluation (anglicky)

CHALOUPKA, Jakub.
Parallel Algorithms for Mean-Payoff Games: An Experimental Evaluation. In Algorithms - European Symposium on Algorithms (ESA) 2009. Berlin : Springer Berlin / Heidelberg, 2009. ISBN 978-3-642-04127-3, s. 599-610. 2009, Kodaň.

více

 
Quantitative Model Checking of Systems with Degradation (anglicky)

BARNAT, Jiří - ČERNÁ, Ivana - TŮMOVÁ, Jana.
Quantitative Model Checking of Systems with Degradation. In 2009 Sixth International Conference on the Quantitative Evaluation of Systems. Los Alamitos (California) : IEEE Computer Society, 2009. ISBN 978-0-7695-3808-2, s. 21-30. 2009, Budapest, Hungary.

více

 
Reachability is decidable for weakly extended process rewrite systems (anglicky)

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, Nizozemsko. ISSN 0890-5401, 2009, vol. 207, no. 6, s. 671-680.

více

 
 
 
nahoru