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
2006
-
Model Checking of RegCTL
Computing and Informatics, year: 2006, volume: 25, edition: 1
-
On Alternative Construction of LTL Tableau
2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006), year: 2006
-
On Combining Partial Order Reduction with Fairness Assumptions
Proceedings of the 11th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2006), year: 2006
-
On Decidability of LTL Model Checking for Process Rewrite Systems
FSTTCS 2006: 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings, year: 2006
-
On Decidability of LTL Model Checking for Weakly Extended Process Rewrite Systems
Year: 2006, type: R&D Presentation
-
Parallel Algorithms for Finding SCCs in Implicitly Given Graphs
Proceedings of the 5th International Workshop on Proceedings of 5th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2006), year: 2006
-
Refining Undecidability Border of Weak Bisimilarity.
Proceedings of the 7th International Workshop on Verification of Infinite-State Systems (INFINITY'05), year: 2006
-
Routing and Level 2 Addressing in a Hardware Accelerator for Network Applications
ICT 2006, 13th International Conference on Telecommunications, year: 2006
-
Special Issue on Parallel and Distributed Verification - Foreword
Formal Methods in System Design, year: 2006, volume: 29, edition: 2
-
Test Input Generation for Java Containers using State Matching
International Symposium on International Symposium on Software Testing and Analysis, year: 2006