@conference {322, title = {Incremental Verification by SMT-based Summary Repair}, booktitle = {20th conference on FORMAL METHODS in COMPUTER-AIDED DESIGN {\textendash} FMCAD 2020}, year = {2020}, publisher = {IEEE digital library, TU Wien Academic Press}, organization = {IEEE digital library, TU Wien Academic Press}, isbn = {978-3-85448-042-6}, url = {http://verify.inf.usi.ch/sites/default/files/upprover-fmcad20.pdf}, author = {Sepideh Asadi and Martin Blicha and Antti E. J. Hyv{\"a}rinen and Grigory Fedyukovich and Natasha Sharygina} } @conference {183, title = {Incremental Verification of Compiler Optimizations}, booktitle = {NASA Formal Methods (NFM)}, year = {2014}, address = {Houston, Texas, USA}, abstract = {
Optimizations are widely used along the lifecycle of software.\ However, proving the equivalence between original and optimized versions is difficult. In this paper, we propose a technique to incrementally\ verify different versions of a program with respect to a fixed property. We\ exploit a safety proof of a program given by a safe inductive invariant.\ For each optimization, such invariants are adapted to be a valid safety\ proof of the optimized program (if possible). The cost of the adaptation depends on the impact of the optimization and is often less than\ an entire re-verification of the optimized program. We have developed a\ preliminary implementation of our technique in the context of Software\ Model Checking. Our evaluation of the technique on different classes of\ industrial programs and standard LLVM optimizations confirms that the\ optimized programs can be re-verified efficiently.
}, author = {Grigory Fedyukovich and Gurfinkel, A. 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} } @conference {147, title = {Interpolation Properties and SAT-based Model Checking}, booktitle = {11th International Symposium on Automated Technology for Verification and Analysis (ATVA)}, year = {2013}, author = {Gurfinkel, A. and Rollini, S. F. and Natasha Sharygina} } @conference {166, title = {Interpolation-based model checking for efficient incremental analysis of software}, booktitle = {IEEE Symposium on Design and Diagnostics of Electronic Circuits and Systems}, year = {2013}, author = {Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen 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 {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} }