The laboratory aims at intensifying the basic and applied research in the area of parallel and distributed methods for the specification, modeling, 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.
University: Masaryk University, Faculty of Informatics
Project: DIVINE 4
Members: Petr Ročkai, Jiří Barnat, Vladimír Štill, Jan Mrázek, Henrich Lauko, Katarína Kejstová
The primary product of the ParaDiSe is DIVINE, an explicit-state model checker for C and C++ programs.Since 2008, Red Hat has contributed to this effort, with the long-term goal of achieving practical, useful results. The particular focus is to build a tool which software engineers could use in their effort to produce correct and reliable software, especially for SMP (multi-core) systems. A next part of this research is on extending usability of DIVINE to codebases with complex build process and on code transformations.