Program analysis and verification tools often rely on state of the art SMT solvers to discharge their core logic first order queries. The design and implementation of such solvers is an active field of research, delivering more mature and performant solvers every year . Nevertheless, current solvers only support a limited number of theories, such as the theories of real arithmetic, strings, and bit-vectors. Other theories, such as the theories of sets, lists, multi-sets, and discrete maps, are still scarcely supported and mainly found in specialised solvers designed for the targeted theory.
JaVerT has at its core a first order solver with support for the theory of real arithmetic and very limited ad-hoc support for the theories of lists and sets. This solver works by encoding the first order fragment of JaVerT logic into Z3 , a world-leading SMT solver developed at Microsoft Research. The **goal** of this thesis is to extend the first order solver of JaVerT with principled support for decidable fragments of the theories of sets and lists (already partially supported) and, for the first time, floating point arithmetic, strings, multi-sets, and discrete maps.
This project combines theory and practice. The limitations of the proposed solver are to be precisely understood and formally characterised and the resulting implementation must be thoroughly evaluated using appropriate test suites.
 D. Monniaux. A Survey on Satisfiability Modulo Theory. CASC'16.
 L. De Moura et al. Z3: An Efficient SMT Solver. TACAS'08.