An SMT-based verification framework for software systems handling arrays, Alberti, Francesco , Faculty of Informatics of the Università della Svizzera Italiana, 02/2015, Volume PhD, Lugano, p.188, (2015)

• Google Scholar
• BibTeX

Symbolic Detection of Assertion Dependencies for Bounded Model Checking, Fedyukovich, Grigory, A. D'Iddio Callia, Hyvärinen Antti E. J., and Sharygina Natasha , 18th International Conference on Fundamental Approaches to Software Engineering (FASE), (2015)

• Google Scholar
• BibTeX

Decision Procedures for Flat Array Properties, Alberti, Francesco, Ghilardi S., and Sharygina Natasha , TACAS, Grenoble, France, (2014)

• Google Scholar
• BibTeX

An extension of lazy abstraction with interpolation for programs with arrays, Alberti, Francesco, Bruttomesso R., Ghilardi S., Ranise S., and Sharygina Natasha , FMSD, (2014)

• Google Scholar
• BibTeX

Incremental Verification of Compiler Optimizations, Fedyukovich, Grigory, Gurfinkel A., and Sharygina Natasha , NASA Formal Methods (NFM), Houston, Texas, USA, (2014)

• Google Scholar
• BibTeX

On Interpolants and Variable Assignments, Jancik, P., Kofronˇ J., Rollini S.F., and Sharygina Natasha , Formal Methods in Computer-Aided Design (FMCAD), Lausanne, Switzerland, (2014)

• Google Scholar
• BibTeX

Towards completeness in Bounded Model Checking through Automatic Recursion Depth Detection, Fedyukovich, Grigory, and Sharygina Natasha , Brazilian Symposium on Formal Methods (SBMF), Maceio, Brazil., (2014)

• Google Scholar
• BibTeX

Verification-Aided Regression Testing, Pastore, F., Mariani L., Hyvärinen Antti E. J., Fedyukovich Grigory, Sharygina Natasha, Sehestedt S., and Muhammad A. , ISSTA, 06/2014, (2014)

• Google Scholar
• BibTeX

VERIGE: Verification with Invariant Generation Engine, Latorre, N., Alberti Francesco, and Sharygina Natasha , SPIN, (2014)

• Google Scholar
• BibTeX

Abstraction and Acceleration in SMT-based Model-Checking for Array Programs, Alberti, Francesco, Ghilardi S., and Sharygina Natasha , CoRR, Volume April 2013, (2013)

• Google Scholar
• BibTeX

Definability of Accelerated Relations in a Theory of Arrays and Its Applications, Alberti, Francesco, Ghilardi S., and Sharygina Natasha , Frontiers of Combining Systems, (2013)

• Google Scholar
• BibTeX

eVolCheck: Incremental Upgrade Checker for C, Fedyukovich, Grigory, Sery O., and Sharygina Natasha , 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), (2013)

• Google Scholar
• BibTeX

Interpolation Properties and SAT-based Model Checking, Gurfinkel, A., Rollini S. F., and Sharygina Natasha , 11th International Symposium on Automated Technology for Verification and Analysis (ATVA), (2013)

• Google Scholar
• BibTeX

Interpolation-based model checking for efficient incremental analysis of software, Fedyukovich, Grigory, Hyvärinen Antti E. J., and Sharygina Natasha , IEEE Symposium on Design and Diagnostics of Electronic Circuits and Systems, (2013)

• Google Scholar
• BibTeX

Loop summarization using state and transition invariants, Kroening, D., Sharygina Natasha, Tonetta S., Tsitovich A., and Wintersteiger C.M. , Formal Methods in System Design, Volume 42, (2013)

• Google Scholar
• BibTeX

A Parametric Interpolation Framework for First-Order Theories, Kovacs, L., Rollini S.F., and Sharygina Natasha , 12th Mexican International Conference on Artificial Intelligence (MICAI), (2013)

• Google Scholar
• BibTeX

PeRIPLO: A Framework for Producing Efficient Interpolants for SAT-based Software Verification, Rollini, S.F., Alt Leonardo, Fedyukovich Grigory, Hyvärinen Antti E. J., and Sharygina Natasha , Logic for Programming Artificial Intelligence and Reasoning (LPAR), Stellenbosch, South Africa, (2013)

• Google Scholar
• BibTeX

PINCETTE - Validating Changes and Upgrades in Networked Software, Chockler, H., Denaro G., Ling M., Fedyukovich Grigory, Hyvärinen Antti E. J., Mariani L., Muhammad A., Oriol M., Rajan A., Sery O., et al. , 17th European Conference on Software Maintenance and Reengineering, (2013)

• Google Scholar
• BibTeX

Resolution Proof Transformation for Compression and Interpolation, Rollini, S.F., Bruttomesso R., Sharygina Natasha, and Tsitovich A. , CoRR, Volume July 2013, (2013)

• Google Scholar
• BibTeX

Using Cross-Entropy for Satisfiability, Chockler, H., Ivrii A., Matsliah A., Rollini S.F., and Sharygina Natasha , ACM Symposium on Applied Computing (SAC), (2013)

• Google Scholar
• BibTeX

An abstraction refinement approach combining precise and approximated techniques, Sharygina, Natasha, Tonetta S., and Tsitovich A. , International Journal on Software Tools for Technology Transfer (STTT), Volume 14, p.1-14, (2012)

• Google Scholar
• BibTeX

FunFrog: Bounded Model Checking with Interpolation-based Function Summarization, Sery, O., Fedyukovich Grigory, and Sharygina Natasha , Tenth International Symposium on Automated Technology for Verification and Analysis (ATVA), Thiruvananthapuram, India, (2012)

• Google Scholar
• BibTeX

Incremental Upgrade Checking by Means of Interpolation-based Function Summaries, Sery, O., Fedyukovich Grigory, and Sharygina Natasha , Twelfth International Conference on Formal Methods in Computer-Aided Design (FMCAD), Cambridge, UK, (2012)

• Google Scholar
• BibTeX

Lazy Abstraction with Interpolants for Arrays, Alberti, Francesco, Bruttomesso R., Ghilardi S., Ranise S., and Sharygina Natasha , 18th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR), Mérida, Venezuela, (2012)

• Google Scholar
• BibTeX

Leveraging Interpolant Strength in Model Checking, Rollini, S.F., Sery O., and Sharygina Natasha , 24th International Conference on Computer Aided Verification (CAV), Berkeley, California, USA, (2012)

• Google Scholar
• BibTeX