Формальная верификация: различия между версиями

м
м (→‎Области применения: викификация)
 
== Теоретические основы ==
 
Верификация представляет собой формальное доказательство на абстрактной математической модели системы, в предположении о том, что соответствие между математической моделью и природой системы считается изначально заданным. Например, по построению модели либо математического анализа и доказательства правильности алгоритмов и программ.
 
Примерами математических объектов, часто используемых для моделирования и формальной верификации программ и систем являются:
 
* формальная семантика языков программирования, например [[операционная семантика]], [[Семантика вычислений#Денотационная семантика|денотационная семантика]], [[аксиоматическая семантика]] ([[логика Хоара]]), [математическая семантика программ].
* [[конечный автомат]]
* помеченная [[модель состояний и переходов]]