Target
Bc. thesis, Master thesis or Research project
Contact

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. 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