Interaktivní verifikace složitého software

• Název práce v češtině: Interaktivní verifikace složitého software
• Název v anglickém jazyce: Interactive Verification of Complex Software
• Akademický rok vypsání: 2016/2017
• Typ práce: disertační práce
• Ústav: Katedra softwarového inženýrství (32-KSI)
• Vedoucí / školitel: RNDr. Filip Zavoral, Ph.D.
• Řešitel: skrytý - zadáno a potvrzeno stud. odd.
• Datum přihlášení: 20.09.2017
• Datum zadání: 20.09.2017
• Datum potvrzení stud. oddělením: 06.10.2017

Zásady pro vypracování

A widely-known problem of many software verification techniques is their scalability. Therefore, the correctness of larger programs is usually checked only using tests, code reviews and other quality assurance processes. In order to prevent, find and fix errors, programmers rely only on their expertise and intuition.
This dissertation aims to make this process more effective by designing novel methods and algorithms based on the state-of-the-art ones, e.g., data flow analysis, abstract interpretation and symbolic execution. Besides using them to verify the program as a whole, they will be mainly used in an interactive fashion. The programmer will utilize them to gather relevant and useful information about a particular problem in the program. For example, under which circumstances can a given variable hold a certain value. An important part of the dissertation is also the efficient implementation of these methods. The impact of the proposed methods and tools will be evaluated on real-world software projects.

Seznam odborné literatury

[1] Pratap Lakshman Tao Xie, Nikolai Tillmann. Advances in unit testing: Theory and practice. In Proc. 38th International Conference on Software Engineering (ICSE 2016), 2016.

[2] Peter Dinges and Gul Agha. Targeted test input generation using symbolic-concrete backward execution. In 29th IEEE/ACM International Conference on Automated Software Engineering (ASE), Västerås, Sweden, September 15-19 2014. ACM.

[3] S. Chandra, S. J. Fink, and M. Sridharan, “Snugglebug: a powerful approach to weakest preconditions,” in PLDI ’09: Proceedings of the 2009 ACM SIGPLAN conference on Programming language design and implementation. New York, NY, USA: ACM, 2009, pp. 363–374.

[4] P. H. Schmitt and B. Weiß. Inferring invariants by symbolic execution. In B. Beckert, editor, VERIFY, volume 259 of CEUR Workshop Proceedings. CEUR-WS.org, 2007.

[5] Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL ’77, pages 238–252, New York, NY, USA, 1977. ACM.

[6] James C. King. Symbolic execution and program testing. Commun. ACM, 19(7):385–394, July 1976.

[7] Gary A. Kildall. A unified approach to global program optimization. In Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL ’73, pages 194–206, New York, NY, USA, 1973. ACM.