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

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

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

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

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

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

• Google Scholar
• BibTeX

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

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

• 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

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

Flexible Interpolation for Efficient Model Checking, Hyvärinen, Antti E. J., Alt Leonardo, and Sharygina Natasha , MEMICS 2016, (2016)

• Google Scholar
• BibTeX

OpenSMT2: An SMT Solver for Multi-Core and Cloud Computing, Hyvärinen, Antti E. J., Marescotti Matteo, Alt Leonardo, and Sharygina Natasha , (2016)

• Google Scholar
• BibTeX

PVAIR: Partial Variable Assignment InterpolatoR, Jančík, Pavel, Alt Leonardo, Fedyukovich Grigory, Hyvärinen Antti E. J., Kofron Jan, and Sharygina Natasha , FASE2016, (2016)

• 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

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

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

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

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

Theory Refinement for Program Verification, Hyvärinen, Antti E. J., Asadi Sepideh, Even Mendoza Karine, Fedyukovich Grigory, Chockler Hana, and Sharygina Natasha , SAT 2017, Melbourne, Australia, (2017)

• Google Scholar
• BibTeX

Computing Exact Worst-Case Gas Consumption for Smart Contracts, Marescotti, Matteo, Blicha Martin, Hyvärinen Antti E. J., Asadi Sepideh, and Sharygina Natasha , International Symposium on Leveraging Applications of Formal Methods ISoLA 2018: Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice , Cyprus, (2018)

• 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

Lattice-Based Refinement in Bounded Model Checking, Even-Mendoza, Karine, Asadi Sepideh, Hyvärinen Antti, Chockler Hana, and Sharygina Natasha , VSTTE, 07/2018, (2018)

• Google Scholar
• BibTeX

Exploiting partial variable assignment in interpolation-based model checking., Jančík, Pavel, Kofron Jan, Alt Leonardo, Fedyukovich Grigory, Hyvärinen Antti E. J., and Sharygina Natasha , Formal Methods in System Design, (2019)

• Google Scholar
• BibTeX