Verificarea formală sau dovada formală este o dovadă formală de conformitate sau neconformitate a subiectului verificării cu descrierea sa formală. Subiectul sunt algoritmi, programe și alte dovezi.
Datorită naturii de rutină chiar și a verificării formale simple și a posibilității teoretice de automatizare completă a acestora, verificarea formală înseamnă de obicei verificare automată folosind un program .
Testarea software-ului nu poate dovedi că un sistem, un algoritm sau un program nu conține erori și defecte și satisface o anumită proprietate. Acest lucru se poate face prin verificare formală .
Verificarea formală poate fi utilizată pentru a verifica sisteme precum software-ul cod sursă, protocoalele criptografice , circuitele logice combinatorii , circuitele digitale cu memorie internă.
Verificarea este o dovadă formală pe un model matematic abstract al sistemului, în ipoteza că corespondența dintre modelul matematic și natura sistemului este considerată inițial dată. De exemplu, pentru a construi un model sau o analiză matematică și o dovadă a corectitudinii algoritmilor și programelor.
Exemple de obiecte matematice folosite adesea pentru modelarea și verificarea formală a programelor și sistemelor sunt:
Există următoarele abordări ale verificării oficiale:
Programarea bazată pe dovezi este o tehnologie folosită în cercurile academice în anii 1980 pentru dezvoltarea de programe pentru calculatoare cu dovezi de corectitudine - dovezi ale absenței erorilor în programe (înțelegerea, în cadrul acestei teorii, a erorilor ca discrepanțe între algoritmul conceput și algoritmul propriu-zis implementat de program).
Dovada poate fi complet automatizată doar pentru un cerc foarte restrâns de teorii simple, așa că devine importantă verificarea sa automată și, pentru aceasta, transformarea într-o formă verificabilă. Un număr semnificativ de probleme practic importante, inclusiv, de exemplu, problema opririi , sunt de nerezolvat din punct de vedere algoritmic .
Pentru a menține rigoarea la verificarea unei dovezi de către un verificator, ar trebui să verificați și verificatorul, pentru care este nevoie de încă un verificator și așa mai departe. Lanțul infinit de verificatori rezultat ar putea fi prăbușit prin construirea unui verificator cu autoverificare care are capacitatea de a se desfășura într-unul practic.