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 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

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

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

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

Accurate Smart Contract Verification through Direct Modelling, Marescotti, Matteo, Otoni Rodrigo, Alt Leonardo, Eugster Patrick, Hyvärinen Antti E. J., and Sharygina Natasha , ISoLA 2020 - 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, (2020)

• 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

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

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

• Google Scholar
• BibTeX

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

• 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

Lattice-based SMT for program verification, Even Mendoza, Karine, Hyvärinen Antti E. J., Chockler Hana, and Sharygina Natasha , International Conference on Formal Methods and Models for System Design, (MEMOCODE), (2019)

• 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