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É
(https://gacr.cz/chyby-v-pocitacovych-programech-mohou-byt-zakerne-a-pritom-tezk
o-odhalitelne/)

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) – hlavní řešitel
Holík Lukáš, doc. Mgr., Ph.D. (UITS)
Kofroň Jan, doc. RNDr., Ph.D.
Křena Bohuslav, Ing., Ph.D. (UITS)
Malásková Věra (UITS)
Peringer Petr, Dr. Ing. (UITS)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
Smrčka Aleš, Ing., Ph.D. (UITS)
Publikace

2020

  • HOLÍK, L.; ROGALEWICZ, A.; VOJNAR, T.; IOSIF, R. Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems. FORMAL METHODS IN SYSTEM DESIGN, 2020, vol. 55, no. 3, p. 137-170. ISSN: 0925-9856. Detail

2019

  • ČEŠKA, M.; JANSEN, N.; JUNGES, S.; KATOEN, J. 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. Praha: Springer International Publishing, 2019. p. 172-190. ISBN: 978-3-030-17464-4. Detail
  • HAVLENA, V.; HOLÍK, L.; LENGÁL, O.; VOJNAR, T. Automata Terms in a Lazy WSkS Decision Procedure (Technical Report). Ithaca: 2019. p. 1-25. Detail
  • HAVLENA, V.; HOLÍK, L.; LENGÁL, O.; VOJNAR, T. Automata Terms in a Lazy WSkS Decision Procedure. In Proceedings of 27th International Conference on Automated Deduction (CADE-27). Lecture Notes in Computer Science. Natal: Springer Verlag, 2019. p. 300-318. ISSN: 0302-9743. Detail
  • HOLÍKOVÁ, L.; JANKŮ, P. Solving String Constraints with Approximate Parikh Image. In Proceedings of EUROCAST'19. Lecture Notes in Computer Science. Heidelberg: Springer International Publishing, 2019. p. 1-8. ISBN: 978-3-030-45092-2. Detail
  • CHEN, Y.; CHIANG, C.; HOLÍK, L.; KAO, W.; LIN, H.; VOJNAR, T.; WEN, Y.; WU, W. J-ReCoVer: Java Reducer Commutativity Verifier. In Proceedings of 17th Asian Symposium on Programming Languages and Systems (APLAS). Lecture Notes in Computer Science. Cham: Springer International Publishing, 2019. p. 357-366. ISBN: 978-3-030-34174-9. Detail
  • KOTOUN, M.; PERINGER, P.; ŠOKOVÁ, V.; VOJNAR, T. PredatorHP Attacks Interval-Sized Regions. Ithaca: 2019. p. 1-4. Detail

2018

  • FIEDOR, J.; MUŽIKOVSKÁ, M.; SMRČKA, A.; VAŠÍČEK, O.; VOJNAR, T. 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. p. 356-359. ISBN: 978-1-4503-5699-2. Detail
  • FIEDOR, T.; HOLÍK, L.; ROGALEWICZ, A.; VOJNAR, T.; SINN, M.; ZULEGER, F. From Shapes to Amortized Complexity. In Proceedings of VMCAI'18. Lecture Notes in Computer Science. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2018. p. 205-225. ISBN: 978-3-319-73720-1. ISSN: 0302-9743. Detail
  • HOLÍK, L.; HOLÍKOVÁ, L. Towards Smaller Invariants for Proving Coverability. In Computer Aided Systems Theory - EUROCAST 2017. Berlin Heidelberg: Springer Verlag, 2018. p. 109-116. ISBN: 978-3-319-74727-9. Detail
  • HRUŠKA, M.; MALÍK, V.; SCHRAMMEL, P.; VOJNAR, T. Template-Based Verification of Heap-Manipulating Programs. In Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design. Austin: FMCAD Inc., 2018. p. 103-111. ISBN: 978-0-9835678-8-2. Detail
  • KŘENA, B.; ŠIMKOVÁ, H.; UR, S.; VOJNAR, T. 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. Las Palmas: Springer International Publishing, 2018. p. 99-108. ISBN: 978-3-319-74726-2. Detail
  • LENGÁL, O.; HEIZMANN, M.; CHEN, Y.; LI, Y.; TSAI, M.; TURRINI, A.; ZHANG, L. Advanced Automata-based Algorithms for Program Termination Checking. In Proceedings of PLDI'18. Philadelphia: Association for Computing Machinery, 2018. p. 135-150. ISBN: 978-1-4503-5698-5. Detail
  • MALÍK, V.; MARTIČEK, Š.; SCHRAMMEL, P.; VOJNAR, T.; SRIVAS, M.; WAHLANG, J. 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. Thessaloniki: Springer International Publishing, 2018. p. 417-421. ISBN: 978-3-319-89962-6. Detail

2017

  • FIEDOR, J.; VOJNAR, T.; SMRČKA, A.; DIAS, R.; FERREIRA, C.; LOURENCO, J.; SOUSA, D. 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. p. 196-206. ISBN: 978-1-5090-6032-0. Detail
  • HRUŠKA, M.; HOLÍK, L.; LENGÁL, O.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T. Forester: From Heap Shapes to Automata Predicates. In Proceedings of TACAS'17. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2017. p. 365-369. ISBN: 978-3-662-54580-5. Detail
  • KOZÁK, D.; KŘENA, B.; ŠIMKOVÁ, H.; VOJNAR, T. 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. p. 25-25. Detail
  • LENGÁL, O.; HONG, C.; CHEN, Y.; MU, S.; SINHA, N.; WANG, B. An Executable Sequential Specification for Spark Aggregation. Ithaca: 2017. Detail
  • LENGÁL, O.; HONG, C.; CHEN, Y.; MU, S.; SINHA, N.; WANG, B. An Executable Sequential Specification for Spark Aggregation. In Proceedings of NETYS'17. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2017. p. 421-438. ISSN: 0302-9743. Detail
  • LENGÁL, O.; CHEN, Y.; TAN, T.; WU, Z. Register Automata with Linear Arithmetic. arXiv:1704.03972: 2017. p. 1-30. Detail
  • LENGÁL, O.; CHEN, Y.; TAN, T.; WU, Z. Register Automata with Linear Arithmetic. In Proceedings of LICS'17. Reykjavik: IEEE Computer Society, 2017. p. 1-12. ISBN: 978-1-5090-3018-7. Detail
  • LENGÁL, O.; VOJNAR, T.; ENEA, C.; SIGHIREANU, M. SPEN: A Solver for Separation Logic. In Proceedings of NFM'17. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2017. p. 302-309. ISBN: 978-3-319-57287-1. Detail
  • ŠIMKOVÁ, H.; KŘENA, B.; VOJNAR, T.; LETKO, Z.; UR, S.; DUDKA, V.; VOLKOVICH, Z.; AVROS, R. Boosted decision trees for behaviour mining of concurrent programmes. Concurrency Computation Practice and Experience, 2017, vol. 29, no. 21, p. 4268-4289. ISSN: 1532-0634. Detail
Produkty

2019

2018

Nahoru