Исследования Microsoft Research в области верификации и тестирования программно-аппаратных комплексов

​Индустрия разработки программного обеспечения постоянно развивается, порождая расширение функциональности и увеличение сложности решений. При этом, требования и ожидания потребителей постоянно растут. Каким же образом можно гарантировать качество, в том числе выполнение определённых свойств, разрабатываемых продуктов?  В настоящем выступлении будут рассмотрены подходы, технологии и инструменты, разработанные в Microsoft Research для решения задач верификации и тестирования свойств программных систем: доказательства свойств путём вывода (Spec#, Z3 и HAVOC); верификации параллельных программ (VCC, Chess и Cuzz); проверки свойств безопасности; верификации драйверов устройств.