Theory-Specific Proof Steps Witnessing Correctness of SMT Executions, Otoni, Rodrigo, Blicha Martin, Eugster Patrick, Hyvärinen Antti E. J., and Sharygina Natasha , DAC 2021 - 58th Design Automation Conference, 11/2021, San Francisco, CA, USA, (2021)

• 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

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

A Solicitous Approach to Smart Contract Verification, Otoni, Rodrigo, Marescotti Matteo, Alt Leonardo, Eugster Patrick, Hyvärinen Antti E. J., and Sharygina Natasha , ACM Transactions on Privacy and Security, (2022)

• 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

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

• Google Scholar
• BibTeX

CHC Model Validation with Proof Guarantees, Otoni, Rodrigo, Blicha Martin, Eugster Patrick, and Sharygina Natasha , 18th International Conference on integrated Formal Methods (iFM23), (2023)

• Google Scholar
• BibTeX

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

• Google Scholar
• BibTeX

Picky CDCL: SMT-solving With Flexible Literal Selection, Britikov, Konstantin I., Hyvärinen Antti E. J., and Sharygina Natasha , VSTTE, (2023)

• 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

Symbolic Model Checking for TLA+ Made Faster, Otoni, Rodrigo, Konnov Igor, Kukovec Jure, Eugster Patrick, and Sharygina Natasha , TACAS - 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Paris, (2023)

• Google Scholar
• BibTeX

Reachability Analysis for Multiloop Programs Using Transition Power Abstraction, Britikov, Konstantin, Blicha Martin, Sharygina Natasha, and Fedyukovich Grigory , FM 24, 09/2024, (2024)

• Google Scholar
• BibTeX

SolTG: A CHC-based Solidity Test Case Generator, Britikov, Konstantin, Zlatkin Ilia, Fedyukovich Grigory, Alt Leonardo, and Sharygina Natasha , Computer Aided Verification, (2024)

• Google Scholar
• BibTeX

CHC-Based Reachability Analysis via Cycle Summarization, Britikov, Konstantin, Fedyukovich Grigory, and Sharygina Natasha , iFM, (2025)

• Google Scholar
• BibTeX

Golem: a flexible and efficient solver for constrained Horn clauses, Blicha, Martin, Britikov Konstantin, and Sharygina Natasha , Formal Methods in System Design, (2025)

• 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

Unsatisfiability Proofs for Horn Solving, Otoni, Rodrigo, Blicha Martin, Rivera Matias Barandiara, Eugster Patrick, Kofron Jan, and Sharygina Natasha , TACAS, (2025)

• Google Scholar
• BibTeX

Validation of CHC Satisfiability with ATHENA, Rodrigo, Otoni, Martin Blicha, Patrick Eugster, and Natasha Sharygina , (2025)

• Google Scholar
• BibTeX

Formally Explaining Neural Network Classification, Sharygina, Natasha, Labbaf Faezeh, Leopardi Fabrizio, Kolárik Tomáš, Fedyukovich Grigory, and Wand Michael , FM 2026, (2026)

• Google Scholar
• BibTeX

Interpreting Logical Explanations of Classifying Neural Networks, Leopardi, Fabrizio, Labbaf Faezeh, Kolárik Tomáš, Wand Michael, and Sharygina Natasha , ESANN 2026, (2026)

• Google Scholar
• BibTeX

Parallel SMT Solving via Iterative Tree Partitioning, Kolárik, Tomáš, Hyvärinen Antti E. J., Asadzadeh Seyedmasoud, and Sharygina Natasha , TACAS 2026, (2026)

• Google Scholar
• BibTeX

Syntactically Convex Model-Based Projection for Linear Real Arithmetic, Becchi, Anna, Fedyukovich Grigory, Gurfinkel Arie, and Nachmanson Lev , TACAS 2026, (2026)

• Google Scholar
• BibTeX