Qed na svobodě: A Survey of Engineering of Formally Verified Software (Přehled inženýrství formálně ověřeného softwaru)

Původní název:

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

Obsah knihy:

Vývoj formálních důkazů správnosti programů může zvýšit skutečnou i vnímanou spolehlivost a usnadnit lepší pochopení specifikací programů a jejich základních předpokladů. Nástroje podporující takový vývoj jsou k dispozici již více než 40 let, ale teprve nedávno se dočkaly širokého praktického využití.

Projekty založené na konstrukci strojově kontrolovaných formálních důkazů nyní dosahují nebývalého rozsahu, srovnatelného s velkými softwarovými projekty, což vede k novým výzvám při vývoji a údržbě důkazů. Navzdory svému rostoucímu významu je oblast důkazového inženýrství zřídkakdy považována za samostatnou oblast; související teorie, techniky a nástroje zahrnují mnoho oblastí a míst. QED at Large pokrývá časovou osu a výzkumnou literaturu týkající se vývoje důkazů pro verifikaci programů, včetně teorií, jazyků a nástrojů.

Zdůrazňuje výzvy a průlomové objevy v každé etapě historie a upozorňuje na výzvy, které jsou v současné době přítomny vzhledem k rostoucímu rozsahu vývoje důkazů. Tato monografie je určena pro výzkumné pracovníky a studenty, kteří se s touto oblastí teprve seznamují.

Poskytuje čtenáři zasvěcený přehled prací, které vedly k moderním technikám formálního ověřování softwaru. V době zvyšující se automatizace je základem mnoha softwarových systémů, takže jsou zdůrazněny i budoucí trendy.