@conference {298, title = {Decomposing Farkas Interpolants}, booktitle = {TACAS}, year = {2019}, author = {Martin Blicha and Antti E. J. Hyv{\"a}rinen and Jan Kofron and Natasha Sharygina} } @conference {277, title = {Duality-Based Interpolation for Quantifier-Free Equalities and Uninterpreted Functions}, booktitle = {17th Conference on Formal Methods in Computer-Aided Design (FMCAD 2017) }, year = {2017}, publisher = {IEEE XPlore and ACM Digital Libraries}, organization = {IEEE XPlore and ACM Digital Libraries}, address = {TU Wien, Vienna, Austria,}, url = {http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD17/fmcad17_proceedings.pdf}, author = {Leonardo Alt and Antti Hyv{\"a}rinen and Sepideh Asadi and Natasha Sharygina} } @article {216, title = {Decision Procedures for Flat Array Properties}, journal = {J. Autom. Reasoning}, volume = {54}, year = {2015}, month = {04/2015}, pages = {352}, chapter = {327}, author = {Francesco Alberti and Ghilardi, S. and Natasha Sharygina} } @conference {185, title = {Decision Procedures for Flat Array Properties}, booktitle = {TACAS}, year = {2014}, publisher = {Springer}, organization = {Springer}, address = {Grenoble, France}, abstract = {
We present new decidability results for quantified fragments\ of theories of arrays. Our decision procedures are fully declarative, parametric in the theories of indexes and elements and orthogonal with respect to known results. We also discuss applications to the analysis of\ programs handling arrays.
}, author = {Francesco Alberti and Ghilardi, S. and Natasha Sharygina} } @conference {167, title = {Definability of Accelerated Relations in a Theory of Arrays and Its Applications}, booktitle = {Frontiers of Combining Systems}, year = {2013}, author = {Francesco Alberti and Ghilardi, S. and Natasha Sharygina} } @conference {155, title = {Detection of Security Vulnerabilities Using Guided Model Checking}, booktitle = {24th International Conference on Logic Programming (ICLP)}, year = {2008}, publisher = {Springer}, organization = {Springer}, address = {Udine, Italy}, author = {Tsitovich, A.} }