Laboratory
The laboratory aims at intensifying the basic and applied research in the area of parallel and distributed methods for the specification, modelling, analysis, and verification of parallel and distributed systems. The mainspring of the research is the development and application of theories which underlie mentioned system development activities. The objective is to bridge the gap between academics and industry by exploiting academically well-founded formal methods and by promoting theory formation in the academic sense on the major issues of selected industrial areas. We want to come-up with practical solutions and tooling to address the needs found in current and innovative development industry projects.Projects
DIVINE is a modern software model checker. Based on the
LLVM toolchain, it can verify programs written in C and C++. The
verification core is built on a foundation of high-performance
algorithms and data structures, and is accompanied by a set of
libraries which provide coverage of the C and C++ standard libraries,
thread support and a large subset of POSIX APIs. DIVINE can use both
explicit and symbolic methods to represent the state space. Finally, it
allows verification of programs under the x86-64 memory model.
RoFI is an open-hardware platform of modular robots. The platform
is designed for building larger robots (RoFIBots) from a small number of
module types. The project deals both with hardware realization and
software solutions. RoFI aims for bridging the gap between theory
(control, synthesis, and reconfiguration) and practice (communication
protocols, software, and hardware implementation).
Contact
Faculty of Informatics / ParaDiSe
Botanicka 68a
Brno, Czech Republic
Phone: +420 549 491 869
http://paradise.fi.muni.cz
Room A416
e-mail: paradise (at) fi.muni.cz