Computing Exact Worst-Case Gas Consumption for Smart Contracts. - Matteo Marescotti; Martin Blicha; Antti E. J. Hyvärinen; Sepideh Asadi; Natasha Sharygina (ISoLA (4), 2018)

Function Summarization Modulo Theories. - Sepideh Asadi; Martin Blicha; Grigory Fedyukovich; Antti E. J. Hyvärinen; Karine Even-Mendoza; Natasha Sharygina; Hana Chockler (LPAR, 2018)

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

Incremental Verification by SMT-based Summary Repair. - Sepideh Asadi; Martin Blicha; Antti E. J. Hyvärinen; Grigory Fedyukovich; Natasha Sharygina (FMCAD, 2020)

Farkas-Based Tree Interpolation. - Sepideh Asadi; Martin Blicha; Antti E. J. Hyvärinen; Grigory Fedyukovich; Natasha Sharygina (SAS, 2020)

A Cooperative Parallelization Approach for Property-Directed k-Induction. - Martin Blicha; Antti E. J. Hyvärinen; Matteo Marescotti; Natasha Sharygina (VMCAI, 2020)

Theory-Specific Proof Steps Witnessing Correctness of SMT Executions. - Rodrigo Otoni; Martin Blicha; Patrick Eugster; Antti E. J. Hyvärinen; Natasha Sharygina (DAC, 2021)

SolCMC: Solidity Compiler's Model Checker. - Leonardo Alt; Martin Blicha; Antti E. J. Hyvärinen; Natasha Sharygina (CAV (1), 2022)

Split Transition Power Abstraction for Unbounded Safety. - Martin Blicha; Grigory Fedyukovich; Antti E. J. Hyvärinen; Natasha Sharygina (FMCAD, 2022)

Summarization of branching loops. - Martin Blicha; Jan Kofron; William Tatarko (SAC, 2022)

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

SMT-based verification of program changes through summary repair. - Sepideh Asadi; Martin Blicha; Antti E. J. Hyvärinen; Grigory Fedyukovich; Natasha Sharygina (Formal Methods Syst. Des., 2022)

Using linear algebra in decomposition of Farkas interpolants. - Martin Blicha; Antti E. J. Hyvärinen; Jan Kofron; Natasha Sharygina (Int. J. Softw. Tools Technol. Transf., 2022)

The Golem Horn Solver. - Martin Blicha; Konstantin Britikov; Natasha Sharygina (CAV (2), 2023)

CHC Model Validation with Proof Guarantees. - Rodrigo Otoni; Martin Blicha; Patrick Eugster; Natasha Sharygina (iFM, 2023)

Reachability Analysis for Multiloop Programs Using Transition Power Abstraction. - Konstantin Britikov; Martin Blicha; Natasha Sharygina; Grigory Fedyukovich (FM (1), 2024)

The FMCAD 2024 Student Forum. - Martin Blicha; Nestan Tsiskaridze (FMCAD, 2024)

Space Explanations of Neural Network Classification. - Faezeh Labbaf; Tomás Kolárik; Martin Blicha; Grigory Fedyukovich; Michael Wand 002; Natasha Sharygina (CAV (3), 2025)

Unsatisfiability Proofs for Horn Solving. - Rodrigo Otoni; Martin Blicha; Matias Barandiaran Rivera; Patrick Eugster; Jan Kofron; Natasha Sharygina (TACAS (2), 2025)

Artifact for the paper Unsatisfiability Proofs for Horn Solving. - Rodrigo Otoni; Martin Blicha; Matias Barandiaran Rivera; Patrick Eugster; Jan Kofron; Natasha Sharygina (Zenodo, 2025)