@conference { FSS_TACAS13, title = {eVolCheck: Incremental Upgrade Checker for C}, booktitle = {19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}, year = {2013}, publisher = {Springer}, organization = {Springer}, author = {Grigory Fedyukovich and Sery, O. and Natasha Sharygina} } @conference {165, title = {PINCETTE - Validating Changes and Upgrades in Networked Software}, booktitle = {17th European Conference on Software Maintenance and Reengineering}, year = {2013}, author = {Chockler, H. and Denaro, G. and Ling, M. and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Mariani, L. and Muhammad, A. and Oriol, M. and Rajan, A. and Sery, O. and Natasha Sharygina and Tautschnig, M.} } @conference { Ondrej Sery; Gri, title = {FunFrog: Bounded Model Checking with Interpolation-based Function Summarization}, booktitle = {Tenth International Symposium on Automated Technology for Verification and Analysis (ATVA)}, year = {2012}, note = {To appear at the conference. The pdf-version is not final.}, address = {Thiruvananthapuram, India}, author = {Sery, O. and Grigory Fedyukovich and Natasha Sharygina} } @conference { Ondrej Sery; Gri, title = {Incremental Upgrade Checking by Means of Interpolation-based Function Summaries}, booktitle = {Twelfth International Conference on Formal Methods in Computer-Aided Design (FMCAD)}, year = {2012}, note = {To appear at the conference. The pdf-version is not final.}, address = {Cambridge, UK}, author = {Sery, O. and Grigory Fedyukovich and Natasha Sharygina} } @conference {146, title = {Leveraging Interpolant Strength in Model Checking}, booktitle = {24th International Conference on Computer Aided Verification (CAV)}, year = {2012}, publisher = {Springer}, organization = {Springer}, address = {Berkeley, California, USA}, abstract = {

Craig interpolation is a well known method of abstraction successfully used in both hardware and software model checking. The logical strength of interpolants can affect the quality of approximations and consequently the performance of the model checkers. Recently, it was observed that for the same resolution proof a complete lattice of interpolants ordered by strength can be derived.
Most state-of-the-art model checking techniques based on interpolation subject the interpolants to constraints that ensure efficient verification as, for example, in transition relation approximation for bounded model checking, counterexample-guided abstraction refinement and function summarization for software update checking. However, in general, these verification-specific constraints are not satisfied by all possible interpolants.
The paper analyzes the restrictions within the lattice of interpolants under which the required constraints are satisfied. This enables investigation of the effect of the strength of interpolants on the particular techniques, while preserving their soundness. As an additional benefit, combination of this result with proof manipulation procedures allows the use of optimized solvers to generate interpolants of different strengths for various model checking techniques.

}, author = {Rollini, S.F. and Sery, O. and Natasha Sharygina} } @conference {149, title = {Function Summaries in Software Upgrade Checking}, booktitle = {Haifa Verification Conference (HVC)}, year = {2011}, publisher = {Springer}, organization = {Springer}, address = {Haifa Verification Conference (HVC)}, author = {Grigory Fedyukovich and Sery, O. and Natasha Sharygina} } @conference {148, title = {Interpolation-based Function Summaries in Bounded Model Checking}, booktitle = {Haifa Verification Conference (HVC)}, year = {2011}, publisher = {Springer}, organization = {Springer}, address = {Haifa, Israel}, abstract = {

During model checking of software against various specifications,\ it is often the case that the same parts of the program have to be modeled/verified multiple times.\ To reduce the overall verification effort, this paper proposes a new technique that extracts function summaries after the initial successful verification run,\ and then uses them for more efficient subsequent analysis of the other specifications.\ Function summaries are computed as over-approximations using Craig interpolation, a mechanism which is well-known to preserve the most relevant information,\ and thus tend to be a good substitute for the functions that were examined in the previous verification runs.\ In our summarization-based verification approach, the spurious behaviors introduced as a side effect of the over-approximation,\ are ruled out automatically by means of the counter-example guided refinement of the function summaries.\ We implemented interpolation-based summarization in our FunFrog tool, and compared it with several state-of-the-art software model checking tools.\ Our experiments demonstrate the feasibility of the new technique and confirm its advantages on the large programs.

}, author = {Sery, O. and Grigory Fedyukovich and Natasha Sharygina} }