Research Project Results
Automated software verification
| Project Identification: | GA201/06/1338 |
| MU Investigator: | Prof. RNDr. Luboš Brim, CSc. |
| MU Faculty/Unit: | Faculty of Informatics |
| Project Period: | 1/2006 - 12/2008 |
| Investor/Programme: | Czech Science Foundation / Standard Projects- |
Results:
The main objective of the project is to create a theoretical and methodological base for computer-aided and autotic verification and validation of software systems.
Publications:
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š - 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š - Č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.
BOZZELLI, Laura - KŘETÍNSKÝ, Mojmír - ŘEHÁK, Vojtěch - STREJČEK, Jan.
On Decidability of LTL Model Checking for Process Rewrite Systems. Acta informatica, Berlin, Springer-Verlag, Germany. ISSN 0001-5903, 2009, vol. 46, no. 1, pp. 1-28. DOI: 10.1007/s00236-008-0082-3.
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.
Š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, Germany. 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.
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, Germany. 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.
ČERNÁ, Ivana - VAŘEKOVÁ, Pavlína - ZIMMEROVÁ, Barbora.
Component Substitutability via Equivalencies of Component-Interaction Automata. Electronic Notes in Theoretical Computer Science, , Elsevier, Germany. ISSN 1571-0661, 2007, vol. 182, no. 1, pp. 39-55.
BARNAT, Jiří - BRIM, Luboš - ROČKAI, Petr.
DiVinE Multi-Core. 2007.
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.
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, 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 - ČEŠKA, Milan - TŮMOVÁ, Jana.
ProbDiVinE. 2007.
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.
BRIM, Luboš - BARNAT, Jiří.
Tutorial: Parallel Model Checking. In Model Checking Software. Berlin, Heidelberg : Springer-Verlag, 2007. ISBN 978-3-540-73369-0, pp. 2-3. 2007, Berlin, Germany.
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.
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.
Č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.
BRIM, Luboš - LINDEN, Isabelle.
Proceedings of the First International Workshop on Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems (MTCoord 2005). NIzozemsko : Elsevier, 2006. 159 s. ENTCS Volume 150, Issue 1. ISBN 1571-0661.
