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.

Description in English
Automated software verification and bug hunting are a hot topic in both industry and academia. Indeed, they can save a lot of money and, in case of safety-critical software, even human lives. This project aims at new automated methods of static formal verification (based on approaches like symbolic verification or automated abstraction) as well as extrapolating dynamic analysis and advanced testing of programs that use several classes of advanced programming constructions. In particular, the project concentrates on pointer programs, concurrent programs (including cloud programs), and container programs. While these areas are to some degree independent, there is also a lot of overlap among them: On one hand, one needs to consider various combinations of the mentioned constructions (e.g., concurrent pointer programs). On the other hand, one needs to solve similar problems for all of them. An important example of the latter considered in the project is dealing with open programs, i.e., program fragments that the programmers need to verify despite their environment is unknown.

Keywords
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;

Key words in English
formal verification; static analysis; symbolic verification; automated abstraction; dynamic analysis and testing; noise injection; model-based testing; automata; logics; pointer programs; concurrent programs; container programs;

GA17-12465S

Czech

Vojnar Tomáš, prof. Ing., Ph.D. - principal person responsible
Holík Lukáš, doc. Mgr., Ph.D. - fellow researcher
Křena Bohuslav, Ing., Ph.D. - fellow researcher
Malásková Věra - fellow researcher
Peringer Petr, Dr. Ing. - fellow researcher
Rogalewicz Adam, doc. Mgr., Ph.D. - fellow researcher
Smrčka Aleš, Ing., Ph.D. - fellow researcher

Department of Intelligent Systems
- responsible department (23.3.2016 - not assigned)
Automated Analysis and Verification Research Group - VeriFIT
- internal (23.3.2016 - 31.12.2019)
Department of Intelligent Systems
- beneficiary (23.3.2016 - 31.12.2019)

HOLÍK, L.; JANKŮ, P.; VOJNAR, T.; LIN, A.; RUMMER, P.: xx; Sloth: An SMT Solver for String Constraints. xx. URL: https://www.fit.vut.cz/research/product/563/. (Software)
Detail

HOLÍK, L.; HOLÍKOVÁ, L.; VOJNAR, T.: xx; MINA: A Tool for Verification of Programs with an Unbounded Number of Threads. xx. URL: https://www.fit.vut.cz/research/product/559/. (Software)
Detail

MARCIN, V.; HARMIM, D.; PAVELA, O.; VOJNAR, T.; FIEDOR, T.; ROGALEWICZ, A.: xx; VeriFIT Static Analysis Plugins. xx. URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/sa-plugins/. (Software)
Detail

FIEDOR, T.; HOLÍK, L.; ROGALEWICZ, A.; VOJNAR, T.; SINN, M.; ZULEGER, F.: xx; Ranger: A Tool for Bounds Analysis of Heap-Manipulating Programs. xx. URL: https://www.fit.vut.cz/research/product/562/. (Software)
Detail

HOLÍKOVÁ, L.; JANKŮ, P.: xx; PICoSo: An SMT Solver for String Constraints. xx. URL: https://www.fit.vut.cz/research/product/620/. (Software)
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.; CHEN, Y.; TAN, T.; WU, Z. Register Automata with Linear Arithmetic. arXiv:1704.03972: 2017. p. 1-30.
Detail

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

LENGÁL, O.; HONG, C.; CHEN, Y.; MU, S.; SINHA, N.; WANG, B. An Executable Sequential Specification for Spark Aggregation. Ithaca: 2017. 32 p.
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

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. no. 10299, p. 421-438. ISSN: 0302-9743.
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

Š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 AND COMPUTATION-PRACTICE & EXPERIENCE, 2017, vol. 29, no. 21, p. 4268-4289. ISSN: 1532-0634.
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

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

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

Č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

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

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

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

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

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. no. 11716, p. 300-318. ISSN: 0302-9743.
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. no. 10747, p. 205-225. ISBN: 978-3-319-73720-1. ISSN: 0302-9743.
Detail

KOTOUN, M.; PERINGER, P.; ŠOKOVÁ, V.; VOJNAR, T. PredatorHP Attacks Interval-Sized Regions. Ithaca: 2019. p. 1-4.
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

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

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

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

Responsibility: Vojnar Tomáš, prof. Ing., Ph.D.