Bc. thesis, Master thesis or Research project

SMT solvers are the underlying reasoning engines for a wide range of automated reasoning techniques in the verification of software, protocols, distributed systems, etc. 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.
  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.
  4. SMT-LIB
  5. Yaga MCSat-based SMT Solver