Program Verification

• Jan Kofroň
• Pavel Parízek

Applying formal methods, such as code model checking and static analysis, to programs before they are deployed is an important mean to achieve their correctness, or error freedom. We develop and improve both underlying techniques – formalisms and algorithms – and verification tools.

Interested in trying how to verify programs instead of just testing them?

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.

MCSAT-based SMT Solver Yaga

Most of the state-of-the-art SMT solvers are based on CDCL(T) framework. MCSat [1,2] represents a generalized approach which has, however, not been thoroughly explored yet. MCSat is particularly attractive for the applications in interpolation-based model checking [3], a popular technique for automated software verification. The goal of this work is to extend the current version of Yaga SMT solver [5] being developed in the Formal Methods Group at D3S with new modules and functionality. This involves support for theories beyond Linear Real Arithmetic, in particular Linear Integer Arithmetic, Non-Linear Arithmetic, and Uninterpreted Functions. Additional desired extensions include support for incrementality and Craig interpolation. The tool is to be evaluated on the benchmarks from SMT-LIB [4] and compared to the existing state-of-the-art solvers.

Depending on the type of the thesis, a particular extension or a subset of the extensions above will be selected.

1. de Moura, L., Jovanović, D. (2013). A Model-Constructing Satisfiability Calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2013. Lecture Notes in Computer Science, vol 7737. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35873-9_1
2. D. Jovanovic, C. Barrett and L. de Moura, “The design and implementation of the model constructing satisfiability calculus,” 2013 Formal Methods in Computer-Aided Design, 2013, pp. 173-180, doi: 10.1109/FMCAD.2013.7027033.
3. Jovanović, D., Dutertre, B. (2021). Interpolation and Model Checking for Nonlinear Arithmetic. In: Silva, A., Leino, K.R.M. (eds) Computer Aided Verification. CAV 2021. Lecture Notes in Computer Science(), vol 12760. Springer, Cham. https://doi.org/10.1007/978-3-030-81688-9_13
4. SMT-LIB
5. Yaga MCSat-based SMT Solver

LLVM-based Verification Framework Hornix

“The LLVM Project is a collection of modular and reusable compiler and toolchain technologies. Despite its name, LLVM has little to do with traditional virtual machines. The name “LLVM” itself is not an acronym; it is the full name of the project.” [1] Thanks to its open architecture, it is possible to “hook” into the compiling process via custom “passes”, which can be used for transforming of the code (even already optimized) and transform it to a form suitable for verification, e.g., a system of Constrained Horn Clauses (CHC) [2]. Such representation can be passed to CHC solver, e.g., Golem [3], which can decide upon violation of assertions contained within the input program.

While basic functionality has been already implemented, the goal of this project is to extend the current implementation of this toolchain to support more features of input programs, e.g., recursive functions, complex types.

1. LLVM Project
2. Constrained Horn Clauses
3. The Golem Horn Solver

Recent Results and Artifacts