Link bibtex
R. Otoni, M. Blicha, P. Eugster, N. Sharygina:
CHC Model Validation with Proof Guarantees, in iFM 2023, pp. 62-81, 2024
ISBN: 978-3-031-47705-8, DOI: 10.1007/978-3-031-47705-8_4
Link bibtex
K. Britikov, M. Blicha, N. Sharygina, G. Fedyukovich:
Reachability Analysis for Multiloop Programs Using Transition Power Abstraction, in Formal Methods, pp. 558-576, 2024
ISBN: 978-3-031-71162-6, DOI: 10.1007/978-3-031-71162-6_29
Link bibtex
S. Asadi, M. Blicha, A. Hyvärinen, G. Fedyukovich, N. Sharygina:
SMT-based verification of program changes through summary repair, in Formal Methods in System Design, 2023
DOI: 10.1007/s10703-023-00423-0
Link bibtex
M. Blicha, K. Britikov, N. Sharygina:
The Golem Horn Solver, in Computer Aided Verification, pp. 209–223, 2023
ISBN: 978-3-031-37703-7, DOI: 10.1007/978-3-031-37703-7_10
Link bibtex
L. Alt, M. Blicha, A. Hyvärinen, N. Sharygina:
SolCMC: Solidity Compiler’s Model Checker, in Computer Aided Verification, pp. 325-338, 2022
ISBN: 978-3-031-13185-1, DOI: 10.1007/978-3-031-13185-1_16
Link bibtex
M. Blicha, G. Fedyukovich, A. Hyvärinen, N. Sharygina:
Split Transition Power Abstraction for Unbounded Safety, in Proceedings of FMCAD'22, pp. 349-358, 2022
ISBN: 978-3-85448-053-2, DOI: 10.34727/2022/isbn.978-3-85448-053-2_42
Link bibtex
M. Blicha, J. Kofroň, W. Tatarko:
Summarization of branching loops, in Proceedings of the 37th ACM/SIGAPP Symposium on Applied Computing, pp. 1808–1816, 2022
ISBN: 978-1-4503-8713-2, DOI: 10.1145/3477314.3507042
Link bibtex
M. Blicha, G. Fedyukovich, A. Hyvärinen, N. Sharygina:
Transition Power Abstractions for Deep Counterexample Detection, in Tools and Algorithms for the Construction and Analysis of Systems, pp. 524-542, 2022
ISBN: 978-3-030-99524-9, DOI: 10.1007/978-3-030-99524-9_29
Link bibtex
M. Blicha, A. Hyvärinen, J. Kofroň, N. Sharygina:
Using linear algebra in decomposition of Farkas interpolants, in International Journal on Software Tools for Technology Transfer 24(1), pp. 111-125, 2022
DOI: 10.1007/s10009-021-00641-z
Link bibtex
R. Otoni, M. Blicha, P. Eugster, A. Hyvärinen, N. Sharygina:
Theory-Specific Proof Steps Witnessing Correctness of SMT Executions, in 58th ACM/IEEE Design Automation Conference (DAC), pp. 541-546, 2021
DOI: 10.1109/DAC18074.2021.9586272
Link bibtex
M. Blicha, A. Hyvärinen, M. Marescotti, N. Sharygina:
A Cooperative Parallelization Approach for Property-Directed k-Induction, in Verification, Model Checking, and Abstract Interpretation, pp. 270-292, 2020
ISBN: 978-3-030-39322-9, DOI: 10.1007/978-3-030-39322-9_13
Link bibtex
S. Asadi, M. Blicha, A. Hyvärinen, G. Fedyukovich, N. Sharygina:
Farkas-Based Tree Interpolation, in Static Analysis, pp. 357-379, 2020
ISBN: 978-3-030-65474-0, DOI: 10.1007/978-3-030-65474-0_16
Link bibtex
S. Asadi, M. Blicha, A. Hyvärinen, G. Fedyukovich, N. Sharygina:
Incremental Verification by SMT-based Summary Repair, in Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020, 2020
ISBN: 978-3-85448-042-6, DOI: 10.34727/2020/isbn.978-3-85448-042-6
Link bibtex
M. Blicha, A. Hyvärinen, J. Kofroň, N. Sharygina:
Decomposing Farkas Interpolants, in Tools and Algorithms for the Construction and Analysis of Systems, pp. 3-20, 2019
ISBN: 978-3-030-17462-0, DOI: 10.1007/978-3-030-17462-0_1
Link bibtex
M. Marescotti, M. Blicha, A. Hyvärinen, S. Asadi, N. Sharygina:
Computing Exact Worst-Case Gas Consumption for Smart Contracts, in Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice, pp. 450-465, 2018
ISBN: 978-3-030-03427-6, DOI: 10.1007/978-3-030-03427-6_33
Link bibtex
S. Asadi, M. Blicha, G. Fedyukovich, A. Hyvärinen, K. Even-Mendoza, N. Sharygina, H. Chockler:
Function Summarization Modulo Theories, in LPAR-22, pp. 56-75, 2018
DOI: 10.29007/d3bt

Filter