Qed at Large: Un studiu de inginerie a software-ului verificat formal

Titlul original:

Qed at Large: A Survey of Engineering of Formally Verified Software

Conținutul cărții:

Dezvoltarea de dovezi formale ale corectitudinii programelor poate crește fiabilitatea reală și percepută și poate facilita o mai bună înțelegere a specificațiilor programelor și a ipotezelor care stau la baza acestora. Instrumentele care sprijină o astfel de dezvoltare sunt disponibile de peste 40 de ani, dar numai recent au fost utilizate pe scară largă în practică.

Proiectele bazate pe construirea de dovezi formale verificate automat ating în prezent o amploare fără precedent, comparabilă cu marile proiecte de software, ceea ce conduce la noi provocări în dezvoltarea și întreținerea dovezilor. În ciuda importanței sale din ce în ce mai mari, domeniul ingineriei dovezilor este rareori considerat în sine; teoriile, tehnicile și instrumentele aferente acoperă multe domenii și locuri. QED at Large acoperă cronologia și literatura de cercetare referitoare la dezvoltarea de dovezi pentru verificarea programelor, inclusiv teorii, limbaje și instrumente.

Ea pune accentul pe provocările și descoperirile din fiecare etapă istorică și evidențiază provocările care sunt prezente în prezent datorită dimensiunii tot mai mari a dezvoltării probelor. Această monografie este destinată utilizării de către cercetători și studenți care sunt noi în domeniu.

Ea oferă cititorului o perspectivă de ansamblu asupra lucrărilor care au condus la tehnicile moderne de verificare formală a software-ului. În vremuri de automatizare crescândă, acest lucru stă la baza multor sisteme software, astfel încât sunt evidențiate și tendințele viitoare.