Detail projektu

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

Období řešení: 1. 1. 2017 - 31. 12. 2019

Typ projektu: grant

Kód: GA17-12465S

Agentura: Grantová agentura České republiky

Program: Standardní projekty

Název anglicky
ROBUST - veRificatiOn and Bug hUnting for advanced SofTware
Typ
grant
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;

Abstrakt

CHYBY V POČÍTAČOVÝCH PROGRAMECH MOHOU BÝT ZÁKEŘNÉ, A PŘITOM TĚŽKO ODHALITELNÉ

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.

Řešitelé
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT) , hlavní řešitel
Kofroň Jan, doc. RNDr., Ph.D. (MFF UK) , spoluřešitel
Holík Lukáš, doc. Mgr., Ph.D. (UITS FIT VUT)
Křena Bohuslav, Ing., Ph.D. (UITS FIT VUT)
Malásková Věra (UITS FIT VUT)
Peringer Petr, Dr. Ing. (UITS FIT VUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT)
Publikace

2020

  • HOLÍK Lukáš, IOSIF Radu, ROGALEWICZ Adam a VOJNAR Tomáš. Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems. Formal Methods in System Design, roč. 55, č. 3, 2020, s. 137-170. ISSN 0925-9856. Detail

2019

  • HAVLENA Vojtěch, HOLÍK Lukáš, LENGÁL Ondřej a VOJNAR Tomáš. Automata Terms in a Lazy WSkS Decision Procedure. In: Proceedings of 27th International Conference on Automated Deduction (CADE-27). Natal: Springer Verlag, 2019, s. 300-318. ISSN 0302-9743. Detail
  • HAVLENA Vojtěch, HOLÍK Lukáš, LENGÁL Ondřej a VOJNAR Tomáš. Automata Terms in a Lazy WSkS Decision Procedure (Technical Report). Ithaca, 2019. Detail
  • CHEN Yu-Fang, CHIANG Chang-Yi, HOLÍK Lukáš, KAO Wei-Tsung, LIN Hsin-Hung, VOJNAR Tomáš, WEN Yean-Fu a WU Wei-Cheng. J-ReCoVer: Java Reducer Commutativity Verifier. In: Proceedings of 17th Asian Symposium on Programming Languages and Systems (APLAS). Lecture Notes in Computer Science, roč. 11893. Cham: Springer International Publishing, 2019, s. 357-366. ISBN 978-3-030-34174-9. Detail
  • KOTOUN Michal, PERINGER Petr, ŠOKOVÁ Veronika a VOJNAR Tomáš. PredatorHP Attacks Interval-Sized Regions. Ithaca, 2019. Detail
  • ČEŠKA Milan, JANSEN Nils, JUNGES Sebastian a KATOEN Joost-Pieter. Shepherding Hordes of Markov Chains. In: Proceedings of 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, roč. 11428. Praha: Springer International Publishing, 2019, s. 172-190. ISBN 978-3-030-17464-4. Detail
  • HOLÍKOVÁ Lenka a JANKŮ Petr. Solving String Constraints with Approximate Parikh Image. In: Proceedings of EUROCAST'19. Lecture Notes in Computer Science. Heidelberg: Springer International Publishing, 2019, s. 1-8. ISBN 978-3-030-45092-2. Detail

2018

  • MALÍK Viktor, MARTIČEK Štefan, SCHRAMMEL Peter, SRIVAS Mandayam, VOJNAR Tomáš a WAHLANG Johanan. 2LS: Memory Safety and Non-termination (Competition Contribution). In: Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, part 2. Lecture Notes in Computer Science, roč. 10806. Thessaloniki: Springer International Publishing, 2018, s. 417-421. ISBN 978-3-319-89962-6. Detail
  • HEIZMANN Matthias, CHEN Yu-Fang, LENGÁL Ondřej, LI Yong, TSAI Ming-Hsien, TURRINI Andrea a ZHANG Lijun. Advanced Automata-based Algorithms for Program Termination Checking. In: Proceedings of PLDI'18. Philadelphia: Association for Computing Machinery, 2018, s. 135-150. ISBN 978-1-4503-5698-5. Detail
  • FIEDOR Jan, MUŽIKOVSKÁ Monika, SMRČKA Aleš, VAŠÍČEK Ondřej a VOJNAR Tomáš. Advances in the ANaConDA Framework for Dynamic Analysis and Testing of Concurrent C/C++ Programs. In: Proceedings of 27th ACM SIGSOFT International Symposium on Software Testing and Analysis. New York: Association for Computing Machinery, 2018, s. 356-359. ISBN 978-1-4503-5699-2. Detail
  • FIEDOR Tomáš, HOLÍK Lukáš, ROGALEWICZ Adam, SINN Moritz, VOJNAR Tomáš a ZULEGER Florian. From Shapes to Amortized Complexity. In: Proceedings of VMCAI'18. Lecture Notes in Computer Science, roč. 10145. Heidelberg: Springer Verlag, 2018, s. 205-225. ISBN 978-3-319-73720-1. ISSN 0302-9743. Detail
  • KŘENA Bohuslav, PLUHÁČKOVÁ Hana, UR Shmuel a VOJNAR Tomáš. Prediction of Coverage of Expensive Concurrency Metrics Using Cheaper Metrics. In: Computer Aided Systems Theory - EUROCAST 2017. 16th International Conference, Las Palmas de Gran Canaria, Spain, February 19-24, 2017, Revised Selected Papers, Part II, roč. 10672. Las Palmas: Springer International Publishing, 2018, s. 99-108. ISBN 978-3-319-74726-2. Detail
  • HRUŠKA Martin, MALÍK Viktor, SCHRAMMEL Peter a VOJNAR Tomáš. Template-Based Verification of Heap-Manipulating Programs. In: Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design. Austin: FMCAD Inc., 2018, s. 103-111. ISBN 978-0-9835678-8-2. Detail
  • HOLÍK Lukáš a HOLÍKOVÁ Lenka. Towards Smaller Invariants for Proving Coverability. In: Computer Aided Systems Theory - EUROCAST 2017. Berlin Heidelberg: Springer Verlag, 2018, s. 109-116. ISBN 978-3-319-74727-9. Detail

2017

  • 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. 421-438. ISSN 0302-9743. Detail
  • 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. Ithaca, 2017. Detail
  • AVROS Renata, DUDKA Vendula, KŘENA Bohuslav, LETKO Zdeněk, PLUHÁČKOVÁ Hana, UR Shmuel, VOJNAR Tomáš a VOLKOVICH Zeev. Boosted decision trees for behaviour mining of concurrent programmes. Concurrency and Computation: Practice and Experience, roč. 29, č. 21, 2017, s. 4268-4289. ISSN 1532-0634. Detail
  • 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. Lecture Notes in Computer Science, roč. 10206. Heidelberg: Springer Verlag, 2017, s. 365-369. ISBN 978-3-662-54580-5. Detail
  • CHEN Yu-Fang, LENGÁL Ondřej, TAN Tony a WU Zhilin. Register Automata with Linear Arithmetic. In: Proceedings of LICS'17. Reykjavik: IEEE Computer Society, 2017, s. 1-12. ISBN 978-1-5090-3018-7. Detail
  • CHEN Yu-Fang, LENGÁL Ondřej, TAN Tony a WU Zhilin. Register Automata with Linear Arithmetic. arXiv:1704.03972, 2017. Detail
  • KOZÁK David, KŘENA Bohuslav, PLUHÁČKOVÁ Hana a VOJNAR Tomáš. Search-Based Testing Concurrent Java Programs Using the RoadRunner Analysis Framework [poster]. The proceedings of the 12th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Telč, 2017. Detail
  • ENEA Constantin, LENGÁL Ondřej, SIGHIREANU Mihaela a VOJNAR Tomáš. SPEN: A Solver for Separation Logic. In: Proceedings of NFM'17. Lecture Notes in Computer Science, roč. 10227. Heidelberg: Springer Verlag, 2017, s. 302-309. ISBN 978-3-319-57287-1. Detail
  • DIAS Ricardo J., FERREIRA Carla, FIEDOR Jan, LOURENCO Joao, SMRČKA Aleš, SOUSA Diogo J. 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. Detail
Produkty

2019

  • PICoSo: SMT řešič pro řezězcová omezení, software, 2019
    Autoři: Holíková Lenka, Janků Petr Detail
  • Pluginy pro statickou analýzu vyvíjené skupinou VeriFIT, software, 2019
    Autoři: Marcin Vladimír, Harmim Dominik, Pavela Ondřej, Vojnar Tomáš, Fiedor Tomáš, Rogalewicz Adam Detail

2018

  • Lenochod - SMT solver pro řetězcová omezení, software, 2018
    Autoři: Holík Lukáš, Janků Petr, Lin Anthony W., Rummer Philipp, Vojnar Tomáš Detail
  • MINA: Nástroj pro verifikaci programů s neomezeným počtem vláken, software, 2018
    Autoři: Holík Lukáš, Holíková Lenka, Vojnar Tomáš Detail
  • Ranger: Nástroj pro Analýzu Mezí Programů Manipulujících s Haldou, software, 2018
    Autoři: Fiedor Tomáš, Holík Lukáš, Rogalewicz Adam, Sinn Moritz, Vojnar Tomáš, Zuleger Florian Detail
Nahoru