Methods for reduction of Craig's interpolant size using partial variable assignment
| Thesis title in Czech: | Metody pro redukci velikosti interpolantů při použití částečného přiřazení |
|---|---|
| Thesis title in English: | Methods for reduction of Craig's interpolant size using partial variable assignment |
| Key words: | Craigova interpolace, částečné přiřazení proměnných, Tseitinovo kódování, symbolický model checking |
| English key words: | Craig interpolation, partial variable assignment, Tseitin’s encoding, symbolic model checking |
| Academic year of topic announcement: | 2015/2016 |
| Thesis type: | diploma thesis |
| Thesis language: | anglič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: | 17.03.2016 |
| Date of assignment: | 24.03.2016 |
| Confirmed by Study dept. on: | 07.04.2016 |
| Date and time of defence: | 12.09.2016 11:30 |
| Date of electronic submission: | 28.07.2016 |
| Date of submission of printed version: | 28.07.2016 |
| Date of proceeded defence: | 12.09.2016 |
| Opponents: | RNDr. Petr Kučera, Ph.D. |
| Guidelines |
| Craig Interpolants are known to be a proper method of over-approximation of sets of states in program verification. They not only improve the practical computational demands of the model checking, but also allow for analysis of infinite state systems where a direct (explicit) approaches fail. Recently, several methods for optimizing both the size of interpolants and the computational time have been introduced. One of them exploits partial variable assignment focusing the interpolant on just a subset of program traces to be considered [3].
The goal of this work is to propose an interpolation system, i.e., a set of interpolation rules, exploiting partial variable assignment with the goal to further reduce the sizes of interpolants, with the aim of preserving important properties usually required by the verification applications, e.g., the path-interpolation property. The interpolation system should be proved to produce correct interpolants and the author is expected to show whether the system yields interpolants having the properties of interest or not and compare the interpolants yielded by the proposed system with existing approaches. |
| References |
| [1] McMillan, K. L. “An Interpolating Theorem Prover.” In Tools and Algorithms for the Construction and Analysis of Systems, edited by Kurt Jensen and Andreas Podelski, 16–30. Lecture Notes in Computer Science 2988. Springer Berlin Heidelberg, 2004. http://link.springer.com/chapter/10.1007/978-3-540-24730-2_2.
[2] Vizel, Y., and O. Grumberg. “Interpolation-Sequence Based Model Checking.” In Formal Methods in Computer-Aided Design, 2009. FMCAD 2009, 1–8, 2009. doi:10.1109/FMCAD.2009.5351148. [3] Jančík P., Kofroň J., Rollini S. F., Sharygina N.: On Interpolants and Variable Assignments, In proc. of Formal Methods in Computer-Aided Design 2014, Lausanne, Switzerland, October 2014 |