Формальная проверка с использованием денотационной семантики?
Это может быть связано с обменом стеками cs или cstheory, но я видел большинство вопросов, помеченных здесь формальной проверкой.
Существует ли обширная литература по использованию денотационной семантики для верификации программы?
С помощью быстрого поиска я нашел
Вольфганг Полак. Проверка программы на основе денотационной семантики. Запись конференции восьмого симпозиума ACM по принципам языков программирования, стр. 149-158. ACM, январь 1981 г.
http://www.pocs.com/Papers/POPL-81.pdf
Основы верификации программы, 2-е издание Жак Лёкс, Курт Зибер ISBN: 978-0-471-91282-8
и этот курс:
https://moves.rwth-aachen.de/teaching/ss-15/sv-sw/
Кроме того, существует ли практический инструмент проверки программ для некоторых языков, использующих денотационную семантику?