String Analysis for Code Contracts
| Thesis title in Czech: | Analýza řetězců v Code Contracts |
|---|---|
| Thesis title in English: | String Analysis for Code Contracts |
| Key words: | řetězce, statická analýza, abstraktní interpretace, Code Contracts |
| English key words: | strings, static analysis, abstract interpretation, Code Contracts |
| Academic year of topic announcement: | 2014/2015 |
| Thesis type: | diploma thesis |
| Thesis language: | angličtina |
| Department: | Department of Distributed and Dependable Systems (32-KDSS) |
| Supervisor: | doc. RNDr. Pavel Parízek, Ph.D. |
| Author: | hidden - assigned and confirmed by the Study Dept. |
| Date of registration: | 16.02.2015 |
| Date of assignment: | 16.02.2015 |
| Confirmed by Study dept. on: | 19.02.2015 |
| Date and time of defence: | 05.09.2016 11:00 |
| Date of electronic submission: | 28.07.2016 |
| Date of submission of printed version: | 28.07.2016 |
| Date of proceeded defence: | 05.09.2016 |
| Opponents: | doc. RNDr. Jan Kofroň, Ph.D. |
| Guidelines |
| Code Contracts is a framework that enables modular verification of .NET programs.
Developers can annotate methods with preconditions, postconditions, and object invariants, and then use a runtime checker or a static checker to verify them. Many interesting properties can be specified and verified using Code Contracts, but the support for strings is currently limited. The goal of this work is to extend the Code Contracts framework to allow for checking properties over strings. First, the candidate has to select relevant and useful string-related properties (e.g., containment) and propose a way for specifying the properties inside Code Contracts. The second major step is the design and implementation of a suitable abstract domain for string expressions, and integration with the existing static checker. Remaining tasks include experimental evaluation, and demonstration of practical usefulness on several example programs. |
| References |
| 1. P. Ferrara, F. Logozzo, M. Fahndrich. Safer Unsafe Code for .NET. OOPSLA 2008, ACM.
2. Source code for the Code Contracts tools for .NET. https://github.com/Microsoft/CodeContracts 3. A.S. Christensen, A. Moeller, and M.I. Schwartzbach. Precise Analysis of String Expressions. SAS 2003, LNCS, vol. 2694. 4. A. Kiezun, V. Ganesh, S. Artzi, P.J. Guo, P. Hooimeijer, and M.D. Ernst. HAMPI: A Solver for Word Equations over Strings, Regular Expressions, and Context-Free Grammars. ACM Transactions on Software Engineering and Methodology, 21(4), 2012. 5. G. Costantini, P. Ferrara, and A. Cortesi. A Suite of Abstract Domains for Static Analysis of String Values. Software: Practice and Experience, 45(2), 2015. |