Верификация программ на ARM ассемблере
В своей прошлой статье я описал процесс верификации примитивной функции на Си. Параллельно привел соображения, почему верификация Си кода недостаточна для того, чтоб считать программу безошибочной. В основном эти соображения сводятся к мысли, что написать код — это только часть истории о получении работающей программы. Следующим приближением к тому, чтобы получить действительно безошибочную программу, является верификация ассемблерных кодов, их уже не нужно будет транслировать и поэтому полностью исключится обширное поле для возникновения ошибок. В данной статье я опишу процесс доказательства некоторых свойств уже для ассемблерного кода, который на порядок примитивней, чем даже простейшая функция на Си, о которой говорилось в прошлой статье.Читать дальше →
