Формальна верифікація
Недавно почав цікавитись формально верифікацією та формальними методами.
Хтось може поділитись реальними сценаріями де це і як використовувалось?
Також, можливо літературою на цю тему і дискретну математику?
Facebook
Twitter
LinkedIn
Yuriy Pitometsu
Ruslan Shevchenko
это довольно большая тема. Есть верификация моделей, есть верификация кода. Даже не очень понятно что посоветовать, если неясно, какие задачи надо решать. Ну, наверное можно посоветовать ознакомиться с каким-то прувером (самый распостраненный — coq, но есть и другие) и попытаться сформировать свою задачу, читая статьи о том, что сделано. Линка с которой можно начать: coq.inria.fr/related-tools
дякую.
мене більш цікавить як зробити модель і верифікнути її. і під моделю я хочу бачити якийсь більш-менш реальний функціонал. Наприклад, логін форма
Alexandr Sova
Для начала поробуй описать эту логин форму как предикат который в последствии будешь доказывать. Как получится тогда уже можно искать подходящий формальный прувер.
Ігор Ковальчук
Я этим не занимаюсь и не разбираюсь, но недавно попался вот такой линк, текста там много „разного”, поэтому, думаю, стоит читать то, что касается 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.”
P.S. И еще может быть это (комментарии) — codingismycraft.com/...l-skill-for-a-programmer ,
интересная ссылка с той же страницы project-everest.github.io .
5 коментарів
Додати коментар Підписатись на коментаріВідписатись від коментарів