Репутація українського ІТ. Пройти опитування Асоціації IT Ukraine
×Закрыть

Формальна верифікація

Недавно почав цікавитись формально верифікацією та формальними методами.
Хтось може поділитись реальними сценаріями де це і як використовувалось?

Також, можливо літературою на цю тему і дискретну математику?

LinkedIn
Допустимые теги: blockquote, a, pre, code, ul, ol, li, b, i, del.
Ctrl + Enter
Допустимые теги: blockquote, a, pre, code, ul, ol, li, b, i, del.
Ctrl + Enter

это довольно большая тема. Есть верификация моделей, есть верификация кода. Даже не очень понятно что посоветовать, если неясно, какие задачи надо решать. Ну, наверное можно посоветовать ознакомиться с каким-то прувером (самый распостраненный — coq, но есть и другие) и попытаться сформировать свою задачу, читая статьи о том, что сделано. Линка с которой можно начать: coq.inria.fr/related-tools

дякую.
мене більш цікавить як зробити модель і верифікнути її. і під моделю я хочу бачити якийсь більш-менш реальний функціонал. Наприклад, логін форма

Для начала поробуй описать эту логин форму как предикат который в последствии будешь доказывать. Как получится тогда уже можно искать подходящий формальный прувер.

Я этим не занимаюсь и не разбираюсь, но недавно попался вот такой линк, текста там много „разного”, поэтому, думаю, стоит читать то, что касается TLA+

www.theatlantic.com/...​e-world-from-code/540393

Цитата:
„Newcombe and his colleagues at Amazon would go on to use TLA+ to find subtle, critical bugs in major systems, including bugs in the core algorithms behind S3” ... „Engineers at the European Space Agency used it to rewrite, with 10 times less code, the operating system of a probe that was the first to ever land softly on a comet. Intel uses it regularly to verify its chips.”

en.wikipedia.org/wiki/TLA

P.S. И еще может быть это (комментарии) — codingismycraft.com/...​l-skill-for-a-programmer ,
интересная ссылка с той же страницы project-everest.github.io .

Подписаться на комментарии