ROBUST - Verifikace a hledání chyb v pokročilém softwaru

Název v angličtině:ROBUST - veRificatiOn and Bug hUnting for advanced SofTware
Hlavní řešitel:Vojnar Tomáš
Spoluřešitelé:Kofroň Jan (MFF UK)
Další řešitelé:Holík Lukáš, Křena Bohuslav, Malásková Věra, Peringer Petr, Rogalewicz Adam, Smrčka Aleš
Agentura:Grantová agentura České republiky - Standardní projekty
Kód:17-12465S
Zahájení:2017-01-01
Ukončení:2019-12-31
Klíčová slova:formální verifikace; statická analýza; symbolická verifikace; automatizovaná abstrakce; dynamická analýza a testování; vkládání šumu; testování řízené modelem; automaty; logiky; programy s ukazateli; paralelní programy; programy s kontejnery;
Anotace:
Automatizovaná verifikace a vyhledávání chyb v softwaru patří mezi témata aktivně řešená jak na univerzitách tak v průmyslu. Konečně tyto techniky mohou ušetřit značné finanční prostředky a u bezpečnostně kritických aplikací také lidské životy. Cílem tohoto projektu jsou nové automatizované metody statické formální verifikace (založené na metodách jako symbolická verifikace či automatická abstrakce) i extrapolující dynamické analýzy a pokročilého testování, a to pro programy používající několik různých pokročilých programovacích technik. Konkrétně se projekt zaměřuje na programy s ukazateli, paralelní programy (včetně cloudových) a programy s kontejnery. Tyto oblasti jsou sice částečně nezávislé, ale také se do značné míry překrývají: Na jednu stranu je zapotřebí zvládnout různé kombinace uvedených konstrukcí (např. paralelní programy s ukazateli) a na druhou stranu je zapotřebí ve všech těchto oblastech řešit podobné problémy. Důležitým příkladem takového problému, který bude řešen v projektu, je potřeba verifikovat otevřené programy, tedy fragmenty kódu, jejichž okolí není známo.

Publikace

2017ENEA Constantin, LENGÁL Ondřej, SIGHIREANU Mihaela a VOJNAR Tomáš. SPEN: A Solver for Separation Logic. In: Proceedings of NFM'17. Heidelberg: Springer Verlag, 2017, s. 302-309. ISSN 0302-9743.
 FIEDOR Jan, LOURENCO Joao, SMRČKA Aleš a VOJNAR Tomáš. Verifying Concurrent Programs Using Contracts. In: 2017 IEEE International Conference on Software Testing, Verification and Validation (ICST). Tokyo: Institute of Electrical and Electronics Engineers, 2017, s. 196-206. ISBN 978-1-5090-6032-0.
 HONG Chih-Duo, CHEN Yu-Fang, LENGÁL Ondřej, MU Shin-Cheng, SINHA Nishant a WANG Bow-Yaw. An Executable Sequential Specification for Spark Aggregation. In: Proceedings of NETYS'17. Heidelberg: Springer Verlag, 2017, s. 1-15. ISSN 0302-9743.
 HRUŠKA Martin, HOLÍK Lukáš, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří a VOJNAR Tomáš. Forester: From Heap Shapes to Automata Predicates. In: Proceedings of TACAS'17. Heidelberg: Springer Verlag, 2017, s. 365-369. ISBN 978-3-662-54580-5.
 CHEN Yu-Fang, LENGÁL Ondřej, TAN Tony a WU Zhilin. Register Automata with Linear Arithmetic. In: Proceedings of LICS'17. XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX, 2017, s. 1-12.
 CHEN Yu-Fang, LENGÁL Ondřej, TAN Tony a WU Zhilin. Register Automata with Linear Arithmetic. arXiv:1704.03972, 2017.

Vaše IPv4 adresa: 54.82.81.154
Přepnout na IPv6 spojení

DNSSEC [dnssec]