Lucrarea prezintă o modalitate în care se poate realiza verificarea automată a corectitudinii programelor scrise în limbaje imperative. Pornind de la noțiunile teoretice necesare inițierii în domeniu (logica Floyd-Hoare [1]), se prezintă o implementare în limbajul CAML Light a unui verificator de programe care este format din două funcții principale: un demonstrator de teoreme (a) şi un generator de condiţii de verificare (b). Programul (algoritmul care se doreşte a fi testat) este furnizat verificatorului de programe, care prin intermediul funcţiei (b), generează o serie de condiţii de verificare, furnizate funcţiei (a) care încearcă să le demonstreze. În caz că reuşeşte, înseamnă că programul este corect. În caz contrar, nu se poate trage nici o concluzie. Un astfel de program este util în practică atunci când o testare exhaustivă a unui algoritm este imposibil de realizat şi este utilizat, mai ales, în domeniul producerii software-ului care controlează activități potenţial dăunătoare omului (convertirea energiei atomice în energie electrică, ghidarea navetelor spaţiale).