Dolmen / Smtml
Improving the OCaml ecosystem libraries for SMT solving
Over the last two decades, SMT solving has grown significantly in popularity, notably in the formal methods field, where it is heavily relied upon by deductive verification tools and symbolic execution engines used to prove the correctness of programs and find bugs. In the OCaml programming language, two libraries have been developed to provide necessary services for users of SMT solvers. Dolmen provides parsing, type checking, and model verification for the SMT-LIB language, as well as other languages used in automated deduction, and Smtml provides a common frontend for multiple SMT solvers, allowing users to easily interact with different solvers and giving them access to features such as query simplification and caching. The purpose of this project is to improve both libraries, as well as their integration, pooling their development efforts together to benefit their users and, more generally, the users of SMT solvers.
- The project's own website: https://github.com/Gbury/dolmen
Run by OCamlPro
This project was funded through the NGI0 Commons Fund, a fund established by NLnet with financial support from the European Commission's Next Generation Internet programme, under the aegis of DG Communications Networks, Content and Technology under grant agreement No 101135429. Additional funding is made available by the Swiss State Secretariat for Education, Research and Innovation (SERI).
