Может ли кто-то подсказать хорошие ресурсы по верификации программ. Сейчас изучаю все преимущественно по статьям(логика хоара, изоморфизм кари-говарда, теория типов). Однако целостного понимания нет. Интетересует вся эта информация в целостном виде(что-то вроде универского курса), и еще желательно с примерами применения, а то понимаешь что это такое, а как воспользоваться - не знаеш.