Decision Procedures for Flat Array Properties, Alberti, Francesco, Ghilardi S., and Sharygina Natasha , J. Autom. Reasoning, 04/2015, Volume 54, Issue 4, p.352, (2015)

• 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

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

SAFARI: SMT-based Abstraction For Arrays with Interpolants, Alberti, Francesco, Bruttomesso R., Ghilardi S., Ranise S., and Sharygina Natasha , 24th International Conference on Computer Aided Verification (CAV), Berkeley, California, USA, (2012)

• Google Scholar
• BibTeX

Lazy Abstraction with Interpolation 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

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

• Google Scholar
• BibTeX

A new Acceleration-based Combination Framework for Array Properties, Alberti, Francesco, Ghilardi Silvio, and Sharygina Natasha , FROCOS 2015, (2015)

• 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

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

Duality-Based Interpolation for Quantifier-Free Equalities and Uninterpreted Functions, Alt, Leonardo, Hyvärinen Antti, Asadi Sepideh, and Sharygina Natasha , 17th Conference on Formal Methods in Computer-Aided Design (FMCAD 2017) , TU Wien, Vienna, Austria,, (2017)

• Google Scholar
• BibTeX

SolCMC: Solidity Compiler’s Model Checker, Alt, Leonardo, Blicha Martin, Hyvärinen Antti E. J., and Sharygina Natasha , CAV, Haifa, Isreal, (2022)

• Google Scholar
• BibTeX

HiFrog: SMT-based Function Summarization for Software Verification, Alt, Leonardo, Asadi Sepideh, Chockler Hana, Even Mendoza Karine, Fedyukovich Grigory, Hyvärinen Antti E. J., and Sharygina Natasha , 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Uppsala, (2017)

• Google Scholar
• BibTeX

A Proof-Sensitive Approach for Small Propositional Interpolants, Alt, Leonardo, Fedyukovich Grigory, Hyvärinen Antti E. J., and Sharygina Natasha , VSTTE 2015, (2015)

• Google Scholar
• BibTeX

LRA Interpolants from No Man's Land, Alt, Leonardo, Hyvärinen Antti E. J., and Sharygina Natasha , Haifa Verification Conference (HVC), (2017)

• Google Scholar
• BibTeX

SMT‑based verification of program changes through summary repair, Asadi, Sepideh, Blicha Martin, Hyvärinen Antti E. J., Fedyukovich Grigory, and Sharygina Natasha , Formal Methods in System Design, 05/2023, (2023)

• Google Scholar
• BibTeX

Function Summarization Modulo Theories, Asadi, Sepideh, Blicha Martin, Fedyukovich Grigory, Hyvärinen Antti E. J., Even-Mendoza Karine, Sharygina Natasha, and Chockler Hana , 22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning, LPAR, Ethiopia, (2018)

• Google Scholar
• BibTeX

Farkas-Based Tree Interpolation, Asadi, Sepideh, Blicha Martin, Hyvärinen Antti, Fedyukovich Grigory, and Sharygina Natasha , SAS 2020 - 27th Static Analysis Symposium, Online Conference, (2020)

• Google Scholar
• BibTeX

Incremental Verification by SMT-based Summary Repair, Asadi, Sepideh, Blicha Martin, Hyvärinen Antti E. J., Fedyukovich Grigory, and Sharygina Natasha , 20th conference on FORMAL METHODS in COMPUTER-AIDED DESIGN – FMCAD 2020, (2020)

• Google Scholar
• BibTeX

Split Transition Power Abstraction for Unbounded Safety, Blicha, Martin, Fedyukovich Grigory, Hyvärinen Antti E. J., and Sharygina Natasha , (2022)

• Google Scholar
• BibTeX

The Golem Horn Solver, Blicha, Martin, Britikov Konstantin, and Sharygina Natasha , Computer Aided Verification, (2023)

• Google Scholar
• BibTeX

A Cooperative Parallelization Approach for Property-Directed k-Induction, Blicha, Martin, Hyvärinen Antti E. J., Marescotti Matteo, and Sharygina Natasha , VMCAI 2020 - 21st International Conference on Verification, Model Checking, and Abstract Interpretation, New Orleans, USA, 19-25 January 2020, (2020)

• Google Scholar
• BibTeX

Transition Power Abstractions for Deep Counterexample Detection, Blicha, Martin, Fedyukovich Grigory, Hyvärinen Antti E. J., and Sharygina Natasha , TACAS, (2022)

• Google Scholar
• BibTeX

Decomposing Farkas Interpolants, Blicha, Martin, Hyvärinen Antti E. J., Kofron Jan, and Sharygina Natasha , TACAS, (2019)

• Google Scholar
• BibTeX

Using linear algebra in decomposition of Farkas interpolants, Blicha, Martin, Hyvärinen Antti E. J., Kofron Jan, and Sharygina Natasha , International Journal on Software Tools for Technology Transfer, (2021)

• Google Scholar
• BibTeX

A Model Checking-based Approach for Security Policy Verification of Mobile Systems, Braghin, C., Sharygina Natasha, and Barone Adesi Katerina , Formal Aspects of Computing Journal, (2010)

• Google Scholar
• BibTeX