Topic of PhD thesis

Advisor:Vojnar Tomáš, prof. Ing., Ph.D.
Student:Hruška Martin, Ing.
Topic:Static Analysis of Heap-Manipulating Programs -- co-supervised by dr. L. Holik
Start:2015/2016
PhD thesis subject:

Statická analýza postavená na formálních základech je moderním a rychle se rozvíjejícím přístupem k ověřování korektnosti počítačových systémů, resp. pro vyhledávání chyb v nich. Existuje a dále se rozvíjí mnoho přístupů k takové analýze či verifikaci: analýza toku dat, pokročilé typové analýzy, abstraktní interpretace, model checking apod. Značná pozornost je těmto přístupům věnována nejen v akademické oblasti, ale také řadou špičkových velkých průmyslových společností (např. IBM, Microsoft, Google, NEC, Red Hat, Facebook apod.) i nově vznikajících spin-off firem (např. Coverity, GrammaTech, MathWorks/AbsInt, Monoidics apod.). Přes tento zájem univerzit i průmyslových společností je však v oblasti statické analýzy stále zapotřebí vyřešit celou řadu teoretických i praktických problémů. Předmětem disertační práce bude konkrétně rozvoj současného stavu v oblasti statické analýzy zaměřené na programy se složitými dynamickými datovými strukturami.

Práce bude řešena ve spolupráci s týmem VeriFIT zabývajícím se na FIT VUT automatizovanou verifikací, zejména pak dr. L. Holíkem, dr. A. Rogalewiczem, Ing. O. Lengálem a Ing. T. Fiedorem. Je zde rovněž možnost úzké spolupráce s různými zahraničními partnery VeriFIT: Uppsala University, Švédsko (prof. P.A. Abdulla, prof. B. Jonsson); Verimag, Grenoble, Francie (dr. R. Iosif), LIAFA, Paříž, Francie (prof. A. Bouajjani, dr. P. Habermehl, dr. M. Sighireanu, dr. C. Enea), Academia Sinica (prof. Y.-F. Cheng) či TU Vídeň, Rakousko (prof. H. Veith, dr. F. Zuleger). Téma je zajímavé také z pohledu spolupráce se společností Red Hat Czech a jeho laboratoří na FIT VUT.

V oblasti statické analýzy programů s dynamickými datovými strukturami má skupina VeriFIT značné zkušenosti s vývojem různých nástrojů (např. Predator či Forester), které získaly řadu ocenění např. na mezinárodní soutěži ve verifikaci software SV-COMP. Konkrétní výzkum v rámci tématu se zaměří na další významné zdokonalení metod, na nichž tyto nástroje stojí, ať už se jedná o techniky založené na automatech, logikách či grafech. Cílem bude mimo jiné umožnit efektivní kombinaci uvedených technik pro práci s dynamickými datovými strukturami s analýzami pro jiné datové typy, umožnit verifikaci neúplných fragmentů programů bez nutnosti modelovat jejich okolí (což je velmi významné pro možnost aplikace uvedených technik na zvlášť kritické části velkých softwarových produktů), umožnit aplikaci uvedených technik v kontextu paralelních programů, umožnit převod programů se složitými datovými strukturami implementovanými pomocí nízkoúrovňových operací na programy s kontejnery apod.

Part of research project:
Related publications:
2014DUDKA Kamil, PERINGER Petr and VOJNAR Tomáš. Predator: A Shape Analyzer Based on Symbolic Memory Graphs (Competition Contribution). In: Tools and Algorithms for the Construction and Analysis of Systems. Heidelberg: Springer Verlag, 2014, pp. 412-414. ISBN 978-3-642-54861-1.
 ENEA Constantin, LENGÁL Ondřej, SIGHIREANU Mihaela and VOJNAR Tomáš. Compositional Entailment Checking for a Fragment of Separation Logic. In: Proceedings of APLAS'14. Heidelberg: Springer Verlag, 2014, pp. 314-333. ISBN 978-3-319-12735-4.
 IOSIF Radu, ROGALEWICZ Adam and VOJNAR Tomáš. Deciding Entailments in Inductive Separation Logic with Tree Automata. In: Proceedings of ATVA'14. Heidelberg: Springer Verlag, 2014, pp. 201-218. ISBN 978-3-319-11935-9.
 MÜLLER Petr and VOJNAR Tomáš. CPAlien: Shape Analyzer for CPAChecker. In: Tools and Algorithms for the Construction and Analysis of Systems. Heidelberg: Springer Verlag, 2014, pp. 395-397. ISBN 978-3-642-54861-1.
2013ABDULLA Parosh A., HAZIZA Frédéric, HOLÍK Lukáš, JONSSON Bengt and REZINE Ahmed. An Integrated Specification and Verification Technique for Highly Concurrent Data Structures. In: 19th International Conference, TACAS 2013. Berlin Heidelberg: Springer Verlag, 2013, pp. 324-338. ISBN 978-3-642-36742-7. ISSN 0302-9743.
 ABDULLA Parosh A., HOLÍK Lukáš, JONSSON Bengt, LENGÁL Ondřej, TRINH Quy Cong and VOJNAR Tomáš. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. In: Proceedings of ATVA'13. Heidelberg: Springer Verlag, 2013, pp. 224-239. ISBN 978-3-319-02443-1.
 DUDKA Kamil, PERINGER Petr and VOJNAR Tomáš. Byte-Precise Verification of Low-Level List Manipulation. In: 20th Static Analysis Symposium. Berlin: Springer Verlag, 2013, pp. 215-237. ISBN 978-3-642-38855-2. ISSN 0302-9743.
 HOLÍK Lukáš, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Fully Automated Shape Analysis Based on Forest Automata. In: Proceedings of CAV'13. Heidelberg: Springer Verlag, 2013, pp. 740-755. ISBN 978-3-642-39798-1. ISSN 0302-9743.