08 февраля 2019
Доклад Шилова Николая Вячеславовича

Уважаемые коллеги!

13 февраля (среда) в 16:00 в 610 аудитории в рамках семинара Регионального математического центра КФУ состоится доклад Шилова Николая Вячеславовича (к.ф.-м.н., доцент), Университет Иннополис, г. Иннополис.

Название доклада: Платформенно-независимая спецификация и верификация стандартных математических функций

Аннотация: Цель проекта "Платформенно-независимый подход к формальной спецификации и верификации стандартных математических функций" - инкрементальный комбинированный подход к спецификации и верификации стандартных математических функций таких как sqrt, cos, sin и так далее.
Платформенно-независимый подход предполагает простую аксиоматизацию машинной арифметики в терминах вещественной арифметики (то есть арифметики поля R вещественных чисел), не фиксируя ни основание системы счисления, ни формат машинного слова. Инкрементальность означает, что спецификация и верификация начинается с рассмотрения наиболее "простого" случая – элементарной спецификации и верификации простого алгоритма, работающего с вещественными числами, а заканчивается модификацией элементарной спецификации и алгоритма для машинной арифметики и верификацией алгоритма, работающего в машинной арифметике. А комбинированность подхода означает, что мы начинаем с рассмотрения "базового случая" - "ручной" верификации (с ручкой и бумагой) для алгоритма, работающего в вещественной арифметике, затем выполняем ручную верификацию алгоритма, работающего в машинной арифметике, используя верификацию для базового случая в качестве "конспекта" (proof-outlines), а заканчиваем - верификацией с использованием автоматизированной системы построения/поиска доказательства для того, чтобы исключить апелляцию к "очевидности" в ручной верификации.
В докладе будет рассказано об основных шагах и результатах платформенно-независимой инкрементальной комбинированной спецификации и верификации стандартных математических функции квадратного корня и синуса. В настоящий момент автоматизированная верификация разработанных алгоритмов выполнена только частично: с использованием системы ACL2 доказано реализуемость (существование) чисел с фиксированной запятой и таблицы начальных приближений квадратного корня.
 

Приглашаем Вас принять участие.

Планируемая дата события: 13.02.2019