Methods for reduction of Craig's interpolant size using partial variable assignment
| Název práce v češtině: | Metody pro redukci velikosti interpolantů při použití částečného přiřazení |
|---|---|
| Název v anglickém jazyce: | Methods for reduction of Craig's interpolant size using partial variable assignment |
| Klíčová slova: | Craigova interpolace, částečné přiřazení proměnných, Tseitinovo kódování, symbolický model checking |
| Klíčová slova anglicky: | Craig interpolation, partial variable assignment, Tseitin’s encoding, symbolic model checking |
| Akademický rok vypsání: | 2015/2016 |
| Typ práce: | diplomová práce |
| Jazyk práce: | anglič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í: | 17.03.2016 |
| Datum zadání: | 24.03.2016 |
| Datum potvrzení stud. oddělením: | 07.04.2016 |
| Datum a čas obhajoby: | 12.09.2016 11:30 |
| Datum odevzdání elektronické podoby: | 28.07.2016 |
| Datum odevzdání tištěné podoby: | 28.07.2016 |
| Datum proběhlé obhajoby: | 12.09.2016 |
| Oponenti: | RNDr. Petr Kučera, Ph.D. |
| Zásady pro vypracování |
| 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. |
| Seznam odborné literatury |
| [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 |