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

 @inproceedings{dort_reference_2020,
    title = {{Reference Mutability for DOT}},
    author = {Dort, Vlastimil and Lhoták, Ondřej},
    year = {2020},
    booktitle = {{Proceedings of 34th European Conference on Object-Oriented Programming}},
    publisher = {Schloss Dagstuhl–Leibniz-Zentrum für Informatik},
    series = {{Leibniz International Proceedings in Informatics (LIPIcs)}},
    location = {Dagstuhl, Germany},
    doi = {10.4230/LIPIcs.ECOOP.2020.18},
    isbn = {978-3-95977-154-2},
    url = {https://drops.dagstuhl.de/opus/volltexte/2020/13175},
    volume = {166},
}
 

 @techreport{dort_reference_report_2020,
    title = {{Reference mutability for DOT – roDOT definitions and proofs}},
    author = {Dort, Vlastimil and Lhoták, Ondřej},
    year = {2020},
    institution = {Department of Distributed and Dependable Systems, Charles University},
    number = {D3S-TR-2020-01},
}
 

 @inproceedings{blicha_cooperative_2020,
    title = {{A Cooperative Parallelization Approach for Property-Directed k-Induction}},
    author = {Blicha, Martin and Hyvärinen, Antti E. J. and Marescotti, Matteo and Sharygina, Natasha},
    year = {2020},
    booktitle = {{Verification, Model Checking, and Abstract Interpretation}},
    editor = {Beyer, Dirk and Zufferey, Damien},
    publisher = {Springer International Publishing},
    series = {{Lecture Notes in Computer Science}},
    location = {Cham},
    doi = {10.1007/978-3-030-39322-9_13},
    isbn = {978-3-030-39322-9},
    pages = {270–292},
}
 

 @inproceedings{asadi_farkasbased_2020,
    title = {{Farkas-Based Tree Interpolation}},
    author = {Asadi, Sepideh and Blicha, Martin and Hyvärinen, Antti E. J. and Fedyukovich, Grigory and Sharygina, Natasha},
    year = {2020},
    booktitle = {{Proceedings of 27th Static Analysis Symposium}},
    url = {https://conf.researchr.org/details/sas-2020/sas-2020-papers/18/Farkas-Based-Tree-Interpolation},
}
 

 @article{blicha_using_2020,
    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 = {2020},
    journal = {{TACAS 2019 Special Issue}},
}
 

 @inproceedings{cizmarik_sharpdetect_2020,
    title = {{SharpDetect: Dynamic Analysis Framework for C#/.NET Programs}},
    author = {Čižmárik, Andrej and Parízek, Pavel},
    year = {2020},
    booktitle = {{Proceedings of the 20th International Conference on Runtime Verification (RV 2020)}},
    publisher = {Springer},
    doi = {10.1007/978-3-030-60508-7_16},
    pages = {298–309},
    url = {https://doi.org/10.1007/978-3-030-60508-7_16},
}
 

 @inproceedings{kapl_endicheck_2020,
    title = {{Endicheck: Dynamic Analysis for Detecting Endianness Bugs}},
    author = {Kápl, Roman and Parízek, Pavel},
    year = {2020},
    booktitle = {{Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020)}},
    publisher = {Springer},
    doi = {10.1007/978-3-030-45237-7_15},
    pages = {254–270},
    url = {https://doi.org/10.1007/978-3-030-45237-7_15},
}
 

 @inproceedings{asadi_incremental_2020,
    title = {{Incremental Verification by SMT-based Summary Repair}},
    author = {Asadi, Sepideh and Blicha, Martin and Hyvärinen, Antti E. J. and Fedyukovich, Grigory and Sharygina, Natasha},
    year = {2020},
    booktitle = {{Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020}},
    editor = {Ivrii, Alexander and Strichman, Ofer},
    publisher = {TU Wien Academic Press},
    series = {{Formal Methods in Computer-Aided Design}},
    doi = {10.34727/2020/isbn.978-3-85448-042-6},
    isbn = {978-3-85448-042-6},
}
 

 @article{jancik_exploiting_2019,
    title = {{Exploiting partial variable assignment in interpolation-based model checking}},
    author = {Jančík, Pavel and Kofroň, Jan and Alt, Leonardo and Fedyukovich, Grigory and Hyvärinen, Antti E. J. and Sharygina, Natasha},
    year = {2019},
    journal = {{Formal Methods in System Design}},
    doi = {10.1007/s10703-019-00342-z},
    issn = {1572-8102},
    url = {https://doi.org/10.1007/s10703-019-00342-z},
}
 

 @article{arcaini_validation_2019,
    title = {{Validation of the Hybrid ERTMS/ETCS Level 3 using Spin}},
    author = {Arcaini, Paolo and Kofroň, Jan and Ježek, Pavel},
    year = {2019},
    journal = {{International Journal on Software Tools for Technology Transfer}},
    doi = {10.1007/s10009-019-00539-x},
    issn = {1433-2787},
    url = {https://doi.org/10.1007/s10009-019-00539-x},
}
 

 @inproceedings{husak_handling_2019,
    title = {{Handling Heap Data Structures in Backward Symbolic Execution}},
    author = {Husák, Robert and Kofroň, Jan and Zavoral, Filip},
    year = {2019},
    booktitle = {{Pre-proceedings for TAPAS 2019}},
    location = {Portugal},
    url = {https://staticanalysis.org/tapas2019/talks/tapas19-pre.pdf},
}
 

 @inproceedings{blicha_decomposing_2019,
    title = {{Decomposing Farkas Interpolants}},
    author = {Blicha, Martin and Hyvärinen, Antti E. J. and Kofroň, Jan and Sharygina, Natasha},
    year = {2019},
    booktitle = {{Tools and Algorithms for the Construction and Analysis of Systems}},
    editor = {Vojnar, Tomáš and Zhang, Lijun},
    publisher = {Springer International Publishing},
    series = {{Lecture Notes in Computer Science}},
    doi = {10.1007/978-3-030-17462-0_1},
    isbn = {978-3-030-17462-0},
    pages = {3–20},
}
 

 @article{parizek_fast_2019,
    title = {{Fast Detection of Concurrency Errors by State Space Traversal with Randomization and Early Backtracking}},
    author = {Parízek, Pavel and Lhoták, Ondřej},
    year = {2019},
    journal = {{International Journal on Software Tools for Technology Transfer}},
    number = {4},
    doi = {10.1007/s10009-018-0484-7},
    issn = {1433-2779},
    pages = {365–400},
    url = {https://link.springer.com/article/10.1007/s10009-018-0484-7},
    volume = {21},
}
 

 @article{husak_askthecode_2019,
    title = {{AskTheCode: Interactive Call Graph Exploration for Error Fixing and Prevention}},
    author = {Husák, Robert and Kofroň, Jan and Zavoral, Filip},
    year = {2019},
    journal = {{Electronic Communications of the EASST}},
    number = {0},
    doi = {10.14279/tuj.eceasst.77.1109},
    issn = {1863-2122},
    url = {https://journal.ub.tu-berlin.de/eceasst/article/view/1109},
    volume = {77},
    shorttitle = {AskTheCode},
}
 

 @inproceedings{parizek_buben_2019,
    title = {{BUBEN: Automated Library Abstractions Enabling Scalable Bug Detection for Large Programs with I/O and Complex Environment}},
    author = {Parízek, Pavel},
    year = {2019},
    booktitle = {{Proceedings of the 17th International Symposium on Automated Technology for Verification and Analysis (ATVA 2019)}},
    publisher = {Springer},
    doi = {10.1007/978-3-030-31784-3_13},
    pages = {228–245},
    url = {https://doi.org/10.1007/978-3-030-31784-3_13},
}
 

Grants and Projects

• 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
• GAČR 14-11384S: Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures