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:

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.

Interested? Contact us: jan.kofron@d3s.mff.cuni.cz

Recent results and artifacts

Link bibtex
P. Parízek:
BUBEN: Automated Library Abstractions Enabling Scalable Bug Detection for Large Programs with I/O and Complex Environment, in Proceedings of the 17th International Symposium on Automated Technology for Verification and Analysis (ATVA 2019), pp. 228-245, 2019
DOI: 10.1007/978-3-030-31784-3_13
Link bibtex
R. Husák, J. Kofroň, F. Zavoral:
AskTheCode: Interactive Call Graph Exploration for Error Fixing and Prevention, in Electronic Communications of the EASST 77(0), 2019
DOI: 10.14279/tuj.eceasst.77.1109
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
P. Arcaini, J. Kofroň, P. Ježek:
Validation of the Hybrid ERTMS/ETCS Level 3 using Spin, in International Journal on Software Tools for Technology Transfer, 2019
DOI: 10.1007/s10009-019-00539-x
Link bibtex
P. Jančík, J. Kofroň, L. Alt, G. Fedyukovich, A. Hyvärinen, N. Sharygina:
Exploiting partial variable assignment in interpolation-based model checking, in Formal Methods in System Design, 2019
DOI: 10.1007/s10703-019-00342-z
Link bibtex
P. Parízek, O. Lhoták:
Fast Detection of Concurrency Errors by State Space Traversal with Randomization and Early Backtracking, in International Journal on Software Tools for Technology Transfer 21(4), pp. 365-400, 2019
DOI: 10.1007/s10009-018-0484-7
Link bibtex
P. Arcaini, P. Ježek, J. Kofroň:
Modelling the Hybrid ERTMS/ETCS Level 3 Case Study in Spin, in Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 277-291, 2018
ISBN: 978-3-319-91271-4, DOI: 10.1007/978-3-319-91271-4_19
PDF bibtex
P. Vysoký, P. Parízek, V. Pech:
INGRID: Creating Languages in MPS from ANTLR Grammars, Technical report no. D3S-TR-2018-01, Department of Distributed and Dependable Systems, Charles University, pp. 1-18, 2018

Grants and Projects