Project information
Techniques for automatic verification and validation of software nad hardware systems
- Project Identification
- 1ET408050503
- Project Period
- 1/2005 - 12/2009
- Investor / Pogramme / Project type
-
Academy of Sciences of the Czech Republic
- Information society (National programme of research)
- MU Faculty or unit
- Faculty of Informatics
- Keywords
- Computer aided and automatic verication, theory and technology of modellingof large systems, methodology of software engineering, embedded systems, parallel and distributed systems, real time systems.
The main objective of the project is to create a theoretical and methodological base for computer-aided and automatic verification and validation of large software and hardware systems. The project aims to support the development of methodologies, technologies and tools of software engineering in automatic and computer-aided verification. The project is to contribute to the research into new technologies for a realistic modelling of large systems, including real-time systems and probabilistic systems, especially with respect to their safety. The aim is to design effective implementations of these models as well as efficient verification technologies based on such models. The project will focus on embedded, distributed and parallel systems. Taking into consideration the complexity of verification processes, the aim is to design methodologies that will make the maximum possible use of new information technologies, such as parallel and distributed computing and hierarchical memories.
Results
Publications
Total number of publications: 94
2012
-
On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties
Science of Computer Programming, year: 2012, volume: 77, edition: 12, DOI
2011
-
Distributed Algorithms for SCC Decomposition
Journal of Logic and Computation, year: 2011, volume: 21, edition: 1, DOI
-
Flash memory efficient LTL model checking
Science of Computer Programming, year: 2011, volume: 76, edition: 2, DOI
2010
-
Scalable shared memory LTL model checking
International Journal on Software Tools for Technology Transfer (STTT), year: 2010, volume: 12, edition: 2, DOI
2009
-
A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties
Formal Methods and Software Engineering, year: 2009
-
BioDiVinE: A Framework for Parallel Analysis of Biological Models
Proceedings of 2nd International Workshop on Computational Models for Cell Processes, year: 2009
-
BioDiVinE: A Tool for Parallel Analysis of Multi-Affine ODE Models
Computational Mehotds in Systems Biology: Abstract of the Posters, year: 2009
-
Can Flash Memory Help in Model Checking?
Formal Methods for Industrial Critical Systems, year: 2009
-
Cluster-Based I/O-Efficient LTL Model Checking
24th IEEE/ACM International Conference on Automated Software Engineering, year: 2009
-
Computational Analysis of Large-Scale Multi-Affine ODE Models
International Workshop on High Performance Computational Systems Biology, year: 2009