Qed at Large: Prehľad inžinierstva formálne overeného softvéru

Pôvodný názov:

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

Obsah knihy:

Vývoj formálnych dôkazov správnosti programov môže zvýšiť skutočnú a vnímanú spoľahlivosť a uľahčiť lepšie pochopenie špecifikácií programov a ich základných predpokladov. Nástroje na podporu takéhoto vývoja sú k dispozícii už viac ako 40 rokov, ale len nedávno sa dočkali širokého praktického využitia.

Projekty založené na konštrukcii strojovo kontrolovaných formálnych dôkazov v súčasnosti dosahujú nebývalý rozsah, porovnateľný s veľkými softvérovými projektmi, čo vedie k novým výzvam pri vývoji a údržbe dôkazov. Napriek svojmu rastúcemu významu sa oblasť dôkazového inžinierstva zriedkakedy považuje za samostatnú; súvisiace teórie, techniky a nástroje pokrývajú mnohé oblasti a miesta. QED at Large pokrýva časovú os a výskumnú literatúru týkajúcu sa vývoja dôkazov na verifikáciu programov vrátane teórií, jazykov a nástrojov.

Zdôrazňuje výzvy a prelomové objavy v každej etape histórie a poukazuje na výzvy, ktoré sú v súčasnosti prítomné vzhľadom na rastúci rozsah vývoja dôkazov. Táto monografia je určená pre výskumníkov a študentov, ktorí sa s touto oblasťou zoznamujú prvýkrát.

Poskytuje čitateľovi zasvätený prehľad prác, ktoré viedli k moderným technikám formálneho overovania softvéru. V čase narastajúcej automatizácie je to základom mnohých softvérových systémov, takže sa poukazuje aj na budúce trendy.