Надійність та безпека інформаційно-керуючих систем критичного призначення суттєво залежать від якості програмного забезпечення (ПЗ), за допомогою якого виконуються критичні функції. Приховані дефекти (дефекти, що не були виявлені при тестуванні та верифікації) критичного ПЗ являються факторами ризику відмови системи. Незалежна верифікація критичного ПЗ, що підтверджує виконання заявлених функцій та дає оцінку вірогідності наявності прихованих дефектів, є необхідною умовою нормативних вимог для різних галузей (МАГАТЕ, Європейська Космічна Агенція ). З цієї точки зору основними проблемами є: надійність незалежної верифікації, оцінювання вірогідності прихованих дефектів, повнота тестового покриття для критичного ПЗ та, як результат, кількісна оцінка функціональної безпеки. Розглядається розробка та використовування вдосконаленої методології доказової незалежної верифікації на базі статичного аналізу вихідних текстів ПЗ для оцінювання семантичних, інтервально-точностних, логічних та інших інваріантів (властивостей ПЗ, які залишаються незмінними по визначенню протягом життєвого циклу ПЗ) критичного ПЗ, а також формування і подання результатів оцінки відповідності ПЗ вимогам стандартів і специфікацій проекту.
