Ověřování asercí kódu pomocí zpětné symbolické exekuce
| Thesis title in Czech: | Ověřování asercí kódu pomocí zpětné symbolické exekuce |
|---|---|
| Thesis title in English: | Code Assertions Verification Using Backward Symbolic Execution |
| Key words: | analýza kódu, verifikace, zpětná symbolická exekuce |
| English key words: | code analysis, verification, backward symbolic execution |
| Academic year of topic announcement: | 2015/2016 |
| Thesis type: | diploma thesis |
| Thesis language: | čeština |
| Department: | Department of Distributed and Dependable Systems (32-KDSS) |
| Supervisor: | doc. RNDr. Jan Kofroň, Ph.D. |
| Author: | hidden - assigned and confirmed by the Study Dept. |
| Date of registration: | 09.06.2016 |
| Date of assignment: | 09.06.2016 |
| Confirmed by Study dept. on: | 09.06.2016 |
| Date and time of defence: | 06.02.2017 10:00 |
| Date of electronic submission: | 06.01.2017 |
| Date of submission of printed version: | 04.01.2017 |
| Date of proceeded defence: | 06.02.2017 |
| Opponents: | doc. RNDr. Pavel Parízek, Ph.D. |
| Guidelines |
| In order to ease the application development process, a lot of technologies and tools have been developed. While some of them aim to provide intuitive inspection and refactoring of the code, the others analyse also the behaviour of the code, looking for possible errors. In the case of C# programming language, tools such as Coverity, Microsoft IntelliTest, and Code Contracts static checker [1] are available.
While these tools can help to build a highly reliable software, the overhead associated with their proper usage in the development process is significant and not affordable by most of software development companies. Therefore, the aim of this thesis is to implement a "light-weight" behaviour verification tool, which works on-demand. The programmer selects a particular assertion in the code, the tool tries to discover any possible program executions violating it, and presents the result in a user-friendly form. In order to be intuitive, the tool will be integrated to the Integrated Development Environment, preferably Microsoft Visual Studio. The tool will presumably use Backward Symbolic Execution, featured for example as a first phase of Symcretic Execution [2]. The tool is expected to support basic C# data types, excluding references and custom data types, because that would be beyond the extent of a master thesis. However, the tool architecture be extensible, allowing for implementation of additional features in the future. |
| References |
| [1] Fahndrich, M.: Static Verification for Code Contracts, In Proceedings of 17th international conference on Static analysis (SAS) 2010
[2] Dinges P., Agha G.: Targeted Test Input Generation Using Symbolic-Concrete Backward Execution, In Proceedings of 29th IEEE/ACM International Conference on Automated Software Engineering (ASE) 2014, ACM, Västerås, Sweden [3] .NET Compiler Platform ("Roslyn"): https://github.com/dotnet/roslyn |