![[rss]](/images/rss.gif)
|
Výběr jazyka Select Language |
|
|
Search |
|
|
Web Stats |
Your IPv4 address: 38.107.191.116 Switch to IPv6 connection DNSSEC  | |
| Info | Team | Projects | Publications | Results |
|---|
Automated Analysis and Verification Research Group - VeriFIT
VeriFIT is a group including researchers and students from FIT BUT interested in research on methods of automated analysis and verification of systems. The group considers both research in the areas of formal verification (model checking, static analysis) and dynamic verification (i.e. verification at run-time, including methods of self-healing) as well as development and evaluation of prototype verification tools.The 2007 Turing award honors E.M. Clark (Carnegie Mellon University), E.A. Emerson (University of Texas at Austin), and J. Sifakis (VERIMAG) for their foundation of model checking. For computer science, the Turing award is an equivalent of the Nobel prize.
Research interests
- Dynamic and formal verification of software, possibilities of self-healing of programs at the run-time (within the European project Shadows).
- Automated verification of infinite-state systems (systems with parameters, recursion, unbounded communication channels, dynamic data structures, etc.) based, e.g., on exploiting the theory of languages and automata.
- Methods of formal verification of hardware, case studies on the network devices being developed in the Liberouter project.
- Methods of formal analysis and verification on object-oriented Petri nets (project PNtalk).
- Verification of (parts of) operating systems: the theme is being prepared (we are looking for people interested to work in this area as well as for those interested in the other areas above, of course).
Seminar
Tool support
Most of the results, published in our papers, include an experimental evaluation on a prototype implementation. Here are some of the tools that we have developed (the others may be provided if you sent us a request by email):
- ARTMC -- a tree-automata based tool for verifying programs operating on complex dynamic data structures linked through pointers.
- VHDL2CA -- a tool for compiling parametric VHDL components into counter automata that may be subsequently used for a formal verification of the components for all possible values of the parameters (using existing tools for formal verification over counter automata).
- Java Race Detector and Healer -- a tool for a run-time detection and automatic healing of race conditions in concurrent Java programs.
- SA -- a tool for computing simulations over labelled transition systems (LTS) and tree automata (TA).
Cooperation
Our group cooperates with many other teams within the Czech republic as well as abroad. For example, we currently cooperate quite actively with:
- LIAFA, Université Paris 7 -- Denis Diderot/CNRS
- VERIMAG, Université Joseph Fourier/INPG/CNRS, Grenoble -- the program verification group
- Department of Information Technology, Uppsala University
- LTA, DISCo, University Milano Bicocca
- IBM Haifa Research Laboratories
- The Cesnet association
- Faculty of informatics, Masaryk University in Brno -- including, e.g., a common doctoral project Mathematical and Engineering Approaches to Developing Reliable and Secure Concurrent and Distributed Computer Systems of the Czech Grant Agency and the MEMICS workshop organized within this project.
© Faculty of Information Technology, BUT, Božetěchova 2,
612 66 Brno, Czech Republic
Tel.: +420 54114 1144, Fax: +420 54114 1270
E-mail: info@fit.vutbr.cz, Web: http://www.fit.vutbr.cz/