Computer Systems Verification

Verification methods

Symbolic techniques and tools (such as SAT and SMT solvers and theorem provers) are used in program verification (establishing interesting properties, such as deadlock absence, race conditions, no assertion violation) to overcome the scaling issues of explicit-state approaches. Some of these methods employ Craig interpolants as an abstract way of representation sets of states. Our research focuses on extending this idea to further improve performance of the verification tools in terms of both verification time and consumed memory.

Project team members wanted!

We seek students willing to participate in our projects focused on (but not restricted to) verification of C programs properties. This involves the following areas:

• Modelling: modelling program semantics (Horn clauses, control-flow graph, logical formulas)
• Model checking: algorithms for model checking (bounded model checking, k-induction, IC3/PDR, Craig interpolation)
• Reasoning engine: SAT solver, SMT solver (extending the algorithms, research on new ones)

Analysis of LLVM passes suitable for software verification

LLVM performs plenty of passes transforming the intermediate representation, usually with the goal to simplify the code for a particular purpose. The goal here is to identify those that contribute to the form being most suitable for software verification. An example of such tools is SeaHorn.

Implementation of new software verification algorithms

This includes development and implementation of new algorithms based on state of the art with the aim to win the software verification competition SV-COMP.

Optimization techniques inside SAT/SMT solver

The goal is to develop algorithms compatible with proof generation and interpolation that improve performance of the solver. This also includes techniques already published in scientific works, but not yet implemented in available tools.

Recent results and artifacts

Grants and Projects

• GAČR 23-06506S: Advanced Analysis and Verification for Advanced Software
• GAČR 20-07487S: Scalable Techniques for Analysis of Complex Properties of Computer Systems
• GAČR 17-12465S: Verification and Bug-Hunting for Advanced Software

 @inproceedings{alt_solcmc_2022,
    title = {{SolCMC: Solidity Compiler’ s Model Checker}},
    author = {Alt, Leonardo and Blicha, Martin and Hyvärinen, Antti E. J. and Sharygina, Natasha},
    year = {2022},
    booktitle = {{Computer Aided Verification}},
    editor = {Shoham, Sharon and Vizel, Yakir},
    publisher = {Springer International Publishing},
    series = {{Lecture Notes in Computer Science}},
    location = {Cham},
    doi = {10.1007/978-3-031-13185-1_16},
    isbn = {978-3-031-13185-1},
    pages = {325--338},
    shorttitle = {SolCMC},
}
 

 @article{asadi_smtbased_2023,
    title = {{SMT-based verification of program changes through summary repair}},
    author = {Asadi, Sepideh and Blicha, Martin and Hyvärinen, Antti E. J. and Fedyukovich, Grigory and Sharygina, Natasha},
    year = {2023},
    journal = {{Formal Methods in System Design}},
    doi = {10.1007/s10703-023-00423-0},
    issn = {1572-8102},
    url = {https://doi.org/10.1007/s10703-023-00423-0},
}
 

 @inproceedings{blicha_golem_2023,
    title = {{The Golem Horn Solver}},
    author = {Blicha, Martin and Britikov, Konstantin and Sharygina, Natasha},
    year = {2023},
    booktitle = {{Computer Aided Verification}},
    editor = {Enea, Constantin and Lal, Akash},
    publisher = {Springer Nature Switzerland},
    series = {{Lecture Notes in Computer Science}},
    location = {Cham},
    doi = {10.1007/978-3-031-37703-7_10},
    isbn = {978-3-031-37703-7},
    pages = {209--223},
}
 

 @inproceedings{blicha_split_2022,
    title = {{Split Transition Power Abstraction for Unbounded Safety}},
    author = {Blicha, Martin and Fedyukovich, Grigory and Hyvärinen, Antti and Sharygina, Natasha},
    year = {2022},
    booktitle = {{Proceedings of FMCAD'22}},
    location = {Trento, Italy},
    doi = {10.34727/2022/isbn.978-3-85448-053-2_42},
    isbn = {978-3-85448-053-2},
    pages = {349--358},
    url = {https://repositum.tuwien.at/handle/20.500.12708/81371},
}
 

 @inproceedings{blicha_summarization_2022,
    title = {{Summarization of branching loops}},
    author = {Blicha, Martin and Kofroň, Jan and Tatarko, William},
    year = {2022},
    booktitle = {{Proceedings of the 37th ACM/SIGAPP Symposium on Applied Computing}},
    publisher = {Association for Computing Machinery},
    series = {{SAC '22}},
    location = {New York, NY, USA},
    doi = {10.1145/3477314.3507042},
    isbn = {978-1-4503-8713-2},
    pages = {1808--1816},
    url = {https://doi.org/10.1145/3477314.3507042},
}
 

 @inproceedings{blicha_transition_2022,
    title = {{Transition Power Abstractions for Deep Counterexample Detection}},
    author = {Blicha, Martin and Fedyukovich, Grigory and Hyvärinen, Antti E. J. and Sharygina, Natasha},
    year = {2022},
    booktitle = {{Tools and Algorithms for the Construction and Analysis of Systems}},
    editor = {Fisman, Dana and Rosu, Grigore},
    publisher = {Springer International Publishing},
    series = {{Lecture Notes in Computer Science}},
    location = {Cham},
    doi = {10.1007/978-3-030-99524-9_29},
    isbn = {978-3-030-99524-9},
    pages = {524--542},
}
 

 @article{blicha_using_2022,
    title = {{Using linear algebra in decomposition of Farkas interpolants}},
    author = {Blicha, Martin and Hyvärinen, Antti E. J. and Kofroň, Jan and Sharygina, Natasha},
    year = {2022},
    journal = {{International Journal on Software Tools for Technology Transfer}},
    number = {1},
    doi = {10.1007/s10009-021-00641-z},
    issn = {1433-2787},
    pages = {111--125},
    url = {https://doi.org/10.1007/s10009-021-00641-z},
    volume = {24},
}
 

 @inproceedings{husak_slicito_2023,
    title = {{Slicito: Using Computational Notebooks for Program Comprehension}},
    author = {Husák, Robert and Kofroň , Jan and Zavoral, Filip},
    year = {2023},
    booktitle = {{2023 IEEE/ACM 31st International Conference on Program Comprehension (ICPC)}},
    doi = {10.1109/ICPC58990.2023.00019},
    pages = {64--68},
    shorttitle = {Slicito},
}
 

 @inproceedings{otoni_theoryspecific_2021,
    title = {{Theory-Specific Proof Steps Witnessing Correctness of SMT Executions}},
    author = {Otoni, Rodrigo and Blicha, Martin and Eugster, Patrick and Hyvärinen, Antti E. J. and Sharygina, Natasha},
    year = {2021},
    booktitle = {{58th ACM/IEEE Design Automation Conference (DAC)}},
    doi = {10.1109/DAC18074.2021.9586272},
    pages = {541--546},
}
 

 @inproceedings{parizek_checking_2023,
    title = {{Checking Just Pairs of Threads for Efficient and Scalable Incremental Verification of Multithreaded Programs}},
    author = {Parízek, Pavel and Kliber, Filip},
    year = {2023},
    booktitle = {{Proceedings of JPF Workshop 2022}},
    publisher = {ACM},
    location = {Michigan, USA},
    doi = {10.1145/3573074.3573082},
    pages = {27--31},
    url = {https://doi.org/10.1145/3573074.3573082},
}
 

 @techreport{parizek_incremental_report_2022,
    title = {{Incremental Verification of Multithreaded Programs by Checking Interleavings for Pairs of Threads}},
    author = {Parízek, Pavel and Kliber, Filip},
    year = {2022},
    institution = {Department of Distributed and Dependable Systems, Charles University},
    number = {D3S-TR-2022-01},
    pages = {1--15},
    url = {http://d3s.mff.cuni.cz/files/public/parizek/pubs/tr-2022-1.pdf},
}