Qed at Large: A Survey of Engineering of Formally Verified Software
A programok helyességére vonatkozó formális bizonyítások kidolgozása növelheti a tényleges és a vélt megbízhatóságot, és megkönnyítheti a programspecifikációk és a mögöttes feltételezések jobb megértését. Az ilyen fejlesztést támogató eszközök már több mint 40 éve rendelkezésre állnak, de csak a közelmúltban kerültek széleskörű gyakorlati használatra.
A gépi ellenőrzésű formális bizonyítások készítésén alapuló projektek mostanában soha nem látott méreteket öltenek, a nagy szoftverprojektekhez hasonlóan, ami új kihívásokhoz vezet a bizonyítások fejlesztése és karbantartása terén. Növekvő jelentősége ellenére a bizonyításelméletet ritkán tekintik önállóan; a kapcsolódó elméletek, technikák és eszközök számos területet és helyszínt érintenek. A QED at Large a programellenőrzéshez szükséges bizonyításfejlesztéssel kapcsolatos idővonalra és kutatási irodalomra terjed ki, beleértve az elméleteket, nyelveket és eszközöket.
Kiemeli a történelem minden egyes szakaszának kihívásait és áttöréseit, és rávilágít a bizonyításfejlesztés egyre nagyobb léptéke miatt jelenleg is jelenlévő kihívásokra. A monográfiát a területen újonnan dolgozó kutatók és hallgatók számára ajánljuk.
Az olvasó számára áttekintő áttekintést nyújt arról a munkáról, amely a szoftverek formális ellenőrzésének mai technikáihoz vezetett. A növekvő automatizálás idején ez számos szoftverrendszer alapját képezi, így a jövőbeli trendek is kiemelésre kerülnek.