Thesis (Selection of subject)Thesis (Selection of subject)(version: 266)
Assignment details
   Login via CAS
Interaktivní verifikace složitého software
Thesis title in Czech: Interaktivní verifikace složitého software
Thesis title in English: Interactive Verification of Complex Software
Academic year of topic announcement: 2016/2017
Type of assignment: dissertation
Thesis language:
Department: Department of Software Engineering (32-KSI)
Supervisor: RNDr. Filip Zavoral, Ph.D.
Author: hidden - assigned and confirmed by the Study Dept.
Date of registration: 20.09.2017
Date of assignment: 20.09.2017
Confirmed by Study dept. on: 06.10.2017
Guidelines
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.
References
[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.
 
Charles University | Information system of Charles University | http://www.cuni.cz/UKEN-329.html