Parallelization and modelling techniques for scalable SMT-based verification, Marescotti, Matteo , Faculty of Informatics, 01.12.2020, Volume PhD, (2020)

• Google Scholar
• BibTeX

Clause Sharing and Partitioning for Cloud-Based SMT Solving, Marescotti, Matteo, Hyvärinen Antti E. J., and Sharygina Natasha , ATVA 2016, (2016)

• Google Scholar
• BibTeX

SMTS: Distributed, Visualized Constraint Solving, Marescotti, Matteo, Hyvärinen Antti E. J., and Sharygina Natasha , {LPAR-22.} 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018, (2018)

• Google Scholar
• BibTeX

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

• Google Scholar
• BibTeX

Space Explanations of Neural Network Classification, Labbaf, Faezeh, Kolárik Tomáš, Blicha Martin, Fedyukovich Grigory, Wand Michael, and Sharygina Natasha , 37th CAV 2025, (2025)

• Google Scholar
• BibTeX

Termination Analysis with Compositional Transition Invariants, Kroening, D., Sharygina Natasha, Tsitovich A., and Wintersteiger C.M. , International Conference on Computer-Aided Verification (CAV), Edinburgh, UK, (2010)

• Google Scholar
• BibTeX

Loopfrog: A Static Analyzer for ANSI-C Programs, Kroening, D., Sharygina Natasha, Tonetta S., Tsitovich A., and Wintersteiger C.M. , The 24th IEEE/ACM International Conference on Automated Software Engineering, Auckland, New Zealand, (2009)

• Google Scholar
• BibTeX

Loop Summarization using Abstract Transformers, Kroening, D., Sharygina Natasha, Tonetta S., Tsitovich A., and Wintersteiger C.M. , 6th International Symposium on Automated Technology for Verification and Analysis (ATVA), Seoul, South Korea, (2008)

• 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

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

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

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

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

Lookahead-Based SMT Solving, Hyvärinen, Antti E. J., Marescotti Matteo, Sadigova Parvin, Chockler Hana, and Sharygina Natasha , LPAR-22, November 2018, Awassa, Ethiopia, (2018)

• Google Scholar
• BibTeX

Search-Space Partitioning for Parallelizing SMT Solvers, Hyvärinen, Antti E. J., Marescotti Matteo, and Sharygina Natasha , SAT 2015, (2015)

• 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

Lookahead in Partitioning SMT, Hyvärinen, Antti E. J., Marescotti Matteo, and Sharygina Natasha , Formal Methods in Computer-Aided Design - FMCAD 2021, Online Conference, (2021)

• 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

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

Function Summaries in Software Upgrade Checking, Fedyukovich, Grigory, Sery O., and Sharygina Natasha , Haifa Verification Conference (HVC), Haifa Verification Conference (HVC), (2011)

• 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

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

Automated Discovery of Simulation Between Programs, Fedyukovich, Grigory, Gurfinkel A., and Sharygina Natasha , LPAR, (2015)

• Google Scholar
• BibTeX