Верификация софта и железа

Для формальной верификации нужна формальная спецификация. Ее для ядра нет (и, ясное дело, не будет), так что тему можно закрывать.

Другое дело, что можно формально проверить, не нарушаются ли некоторые общие и очевидные constraint-ы. Этим для ядра занимается, например, Coverity, результаты анализа они регулярно публикуют. Толку от этого, правда, довольно мало.

Про железо читай тут: http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-91.pdf

Занимается ли кто-нибудь формальной верификацией драйверов или отдельных подсистем линуксового ядра?
метка: verification

Да, вот даже новость на ЛОРе.

Подскажите литературу/блоги/etc, посвященные методам верификации программ и аппаратного обеспечения.

Proceedings of CAV, POPL, LICS и прочих конференций?