dmrpereira / smtada Goto Github PK

Title : SmtAda - A Simple Ada Backend Support Framework for Smt-provers

Author : David Pereira ([email protected])

Short Description:

This SmtAda, a set of Smt-provers bindings to the Ada programming language. The main goal of SmtAda is to provide users with easy access to the power of automated provers when they are writting their Ada code. In this way, the user gains access to powerful logical reasoning methods at the code level, without the need to use formal verification platforms supporting Ada.

This project is still under its first development steps, so no guarantees of the correctness of the code are given. If you find bugs or have suggestions to improvements, non-supported provers of interest, or any other point you wish to make about this project, please send me an email. I will be more than glad to listen to you thoughts!

The currently supported Smt provers are :

• CVC3, and CVC4 ;
• Z3 ;
• Yices 1.

TODO:

• High-level SMT-Lib v2. supports ;
• Support for MathSat, Yices 2, and alt-ergo