Project information
Automated software verification
- Project Identification
- GA201/06/1338
- Project Period
- 1/2006 - 12/2008
- Investor / Pogramme / Project type
-
Czech Science Foundation
- Standard Projects
- MU Faculty or unit
- Faculty of Informatics
- Keywords
- verification, model-checking, software, components
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. 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 software systems, including real-time 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
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
Total number of publications: 45
2006
-
Cluster-Based LTL Model Checking of Large Systems
Formal Methods for Components and Objects, year: 2006
-
Component Substitutability via Equivalencies of Component-Interaction Automata
Pre-proceedings of the International Workshop on Formal Aspects of Component Software (FACS'06), year: 2006
-
Distributed breadth-first search LTL model checking
Formal Methods in System Design, year: 2006, volume: 29, edition: 2
-
Distributed Qualitative LTL Model Checking of Markov Decision Processes
Proceedings of 5th International Workshop on Parallel and Distributed Methods in verifiCation, year: 2006
-
Distributed Verification: Exploring the Power of Raw Computing Power
5th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2006), year: 2006
-
DiVinE -- A Tool for Distributed Verification
Computer Aided Verification, year: 2006
-
DiVinE Library
Year: 2006
-
Experimental Comparison of Algorithms Checking Proviso for Partial Order Reduction
2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006), year: 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