|
|
Effective Automated Software Verification: A Multilayered Approach
Blicha, Martin ; Kofroň, Jan (vedoucí práce) ; Rümmer, Philipp (oponent) ; Bjørner, Nikolaj (oponent)
V posledních letech automatická formální verifikace software pokročila z několika výzkumných laboratoří do rozsáhlých aplikací, jako je cloudová infrastruktura a smart kontrakty. Formální verifikační techniky založené na technice model checking poskytují nezbytné záruky úplným a automatickým zkoumáním chování systémů. Navíc poskytují svědky (vysvětlení) pro výsledek své analýzy: chybové chování, pokud nějaké existuje, nebo důkaz o absenci takového chování. Obecný problém, který se automatická verifikace software snaží vyřešit, je však nerozhodnu- telný. Navzdory této teoretické překážce je v mnoha případech, které se v praxi vyskytují, docela efektivní. Tento (možná překvapivý) úspěch připisujeme kombinaci faktorů: neutuchajícímu úsilí výzkumníků, kteří přicházejí s novými verifikačními postupy pro třídy problémů, kde existující techniky narážejí na své možnosti; úžasný pokrok v základních technologiích řešení splnitel- nosti, zvláště v Satisfiability Modulo Theories (SMT); a zvýšení dostupného výpočetního výkonu prostřednictvím paralelních a cloudových výpočtů. Nicméně rostoucí složitost systémů v reálném světě představuje nové výzvy pro formální verifikace,...
|
host ::
RSS.