@article {351, title = {Exploiting partial variable assignment in interpolation-based model checking.}, journal = {Formal Methods in System Design}, year = {2019}, abstract = {

Craig interpolation has been successfully employed in symbolic program verification as a means of abstraction for sets of program states. In this article, we present the partial variable assignment interpolation system, an extension of the labeled interpolation system, enriched by partial variable assignments. It allows for both generation of smaller interpolants as well as for their faster computation. We present proofs of important properties of the interpolation system as well as a set of experiments proving its usefulness.

}, url = {https://link.springer.com/article/10.1007\%2Fs10703-019-00342-z}, author = {Pavel Jan{\v c}{\'\i}k and Jan Kofron and Leonardo Alt and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @conference {234, title = {PVAIR: Partial Variable Assignment InterpolatoR}, booktitle = {FASE2016}, year = {2016}, url = {http://verify.inf.usi.ch/sites/default/files/main-2.pdf}, author = {Pavel Jan{\v c}{\'\i}k and Leonardo Alt and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Jan Kofron and Natasha Sharygina} } @conference {210, title = {On Interpolants and Variable Assignments}, booktitle = {Formal Methods in Computer-Aided Design (FMCAD)}, year = {2014}, address = {Lausanne, Switzerland}, author = {Jancik, P. and KofronĖ‡, J. and Rollini, S.F. and Natasha Sharygina} }