Kamil Dudka (Red Hat): Static Analysis and Formal Verification at Red Hat
Red Hat uses static analyzers to automatically find bugs in the source code of Red Hat Enterprise Linux. The distribution consists of approx. 3000 RPM packages and 300 million lines of code. Red Hat develops an open source tool that can statically analyze this amount of software in a fully automatic way. We give it source RPM packages of our choice and get the results of selected static analyzers in a unified machine-readable format. This talk will cover which static analyzers are used by Red Hat and how their results are handled. Red Hat is now also experimenting with formal verifiers Symbiotic and Divine, which are developed by research groups of Masaryk University. Is there any chance to integrate such tools into Red Hat’s static analysis workflow?
Jan Fiedor (Honeywell): Verification of Safety-critical Systems at Honeywell
Compared to traditional software development, development of safety-critical systems is different. Beside the source code, we also have the requirements, the model(s) of the system, the blueprints of the hardware components, etc. We also have to follow strict certification guidelines when proving that the final product fulfills the given requirements. Honeywell develops a service that can verify both the requirements and the source code, finding as much problems as possible early by analyzing the requirements and keeping the amount of problems to be found later when verifying the source code to a minimum. This talk will cover some of the approaches that can be used to detect defects in the requirements and the source code, the types of defects in the requirements we are interested in finding, and how to handle various kinds of data we need to work with (requirements, models, source code).