Ověřování asercí kódu pomocí zpětné symbolické exekuce
| Název práce v češtině: | Ověřování asercí kódu pomocí zpětné symbolické exekuce |
|---|---|
| Název v anglickém jazyce: | Code Assertions Verification Using Backward Symbolic Execution |
| Klíčová slova: | analýza kódu, verifikace, zpětná symbolická exekuce |
| Klíčová slova anglicky: | code analysis, verification, backward symbolic execution |
| Akademický rok vypsání: | 2015/2016 |
| Typ práce: | diplomová práce |
| Jazyk práce: | čeština |
| Ústav: | Katedra distribuovaných a spolehlivých systémů (32-KDSS) |
| Vedoucí / školitel: | doc. RNDr. Jan Kofroň, Ph.D. |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 09.06.2016 |
| Datum zadání: | 09.06.2016 |
| Datum potvrzení stud. oddělením: | 09.06.2016 |
| Datum a čas obhajoby: | 06.02.2017 10:00 |
| Datum odevzdání elektronické podoby: | 06.01.2017 |
| Datum odevzdání tištěné podoby: | 04.01.2017 |
| Datum proběhlé obhajoby: | 06.02.2017 |
| Oponenti: | doc. RNDr. Pavel Parízek, Ph.D. |
| Zásady pro vypracování |
| 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. |
| Seznam odborné literatury |
| [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 |