«Практическое руководство Information Technologies to Open Knowledge for Eastern Europe and Central Asia Member of the ...»
Пример истории успеха Who we are KNU – Kyiv National Taras Shevchenko University The cooperation story Project: “Practical Formal Verification Using Automated Reasoning and Model Checking” (2006–2009) Funding Body: EU FP6 (Sixth Framework Programme), INTAS Project budget: 150 000 EURO Partners: Research Institute for Symbolic Computation (Johannes Kepler University, Austria), Research Institute e-Austria (Romania), Glushkov Institute of Cybernetics (Ukraine), Moscow State University (Russia), Vekua Scientific Institute of Applied Mathematics (Georgia).
The first INTAS project “Rewriting Techniques and Efficient Theorem Proving” was carried out at the Faculty of Cybernetics of KNU from 1998 to 2000 and the second one – “Weak Arithmetics” – from 2000 to 2004. It is possible to put that the project presented below was their continuation.
The project addresses one of the current hot topics in Information Technology.
As the complexity of the software and hardware systems increases, and also their use becomes widespread in applications whose reliability is critical (e.g.
secure payments, automotive industry), the use of formal and logical methods in the design and verification of such systems is unavoidable.
The FP6 of the EC, through its IST programme, also put a special emphasis on the use of formal and logical methods in software and hardware design.
That is why the main objective of the project was to advance the state-of-the art in proving and checking techniques for information systems, and to apply them to concrete industrial problems. For this, by using practical problems for testing the different methods for proving and model checking, the project par ticipants had to develop different efficient techniques and identified the most appropriate ones, as well as the necessary adaptations, improvements, and com binations of methods which are more appropriate for solving industrial prob lems. This could be achieved by the joining of efforts of several teams having leading positions in the fields of their investigations relating to the project.
What were our main The special emphasis and the applications of this project are related to the area achievements of improving the reliability of software and hardware design and devices which are used in information technology. The theoretical results include numerous concrete methods for the verification of software and of communication proto cols, some of them being specific to concrete areas of applications. The practi cal results include various tools for: management of mathematical knowledge, natural style interface with proving and checking engines, for proving in spe cial domains which arise in verification and checking, and for verification and static analysis of software. Some of the tools developed in the project are already in use in concrete cooperation with industrial partners, or are available in public repositories. As to KNU, the project permitted also to improve the SAD system (http://nevidal.org/) being developed at the Faculty of Cybernetics, KNU.
Эффективный нетворкинг Lessons • An important result of the project is the increased awareness and learned/Benefits acceptance of formal and logical methods in industry, which in turn has a benefic impact on the reliability of software and hardware systems and information systems in general.
• The partners have a possibility to use the experience from the project, both theoretical and practical, for realizing more efficient tools, includ ing possible commercial ones, and for performing formal verification tasks for industrial users.
• The short-term impacts of the project are:
• use of the experience of each research teams to improve the quality of investigations;
• intensification of cooperation activities in order to submit common proposals for European FP7 calls;
• dissemination of common scientific results.
• The current project long-term impacts are:
• facilitation of the increase of professional experience of all the teams;
• creation of a trust relation necessary for future multi-national proj ects in different branches of IT;
• formation of new specialists in the frame of multi-national programs.
What are our research • Ontology;
areas of interest • Foundations of Computer Science;
• Artificial Intelligence;
• Computational Linguistics;
• Natural Language Processing;
• Automated Reasoning;
• Verification and synthesis;
• Mathematical knowledge management;
• Software development technology;
• Theoretical and applied research in information systems development.
Where you can find us 64, Volodymyrska str., 01601, Kyiv, Ukraine Tel.: (+38) 044 521 35 54, Fax: (+38) 044 259 04 39, Web: www.unicyb.kiev.ua e-mail: email@example.com