Програмна верификация

ПВ е процесът на формално доказване, че една компютърна програма изпълнява точно това, което е заявено по команда и се предполага, че трябва да реализира. Това е свеобразен вид формална верификация, която има за цел да провери самия код на операцията. За някои програмни езици, програмите могат да бъдат проверени чрез логическо равенство и индукция. Код на императивен език може да бъде проверен и доказан, че е коректен чрез логиката на Hoare.