.. SMTFrontEnd documentation master file, created by
   sphinx-quickstart on Fri Mar  1 20:28:56 2013.
   You can adapt this file completely to your liking, but it should at least
   contain the root `toctree` directive.

Welcome to SMTFrontEnd
=======================================

This is a course project for Formal Methods. It aims at designing and implementing a lightweight front end for various SMT solvers. Currently, we are going to support Alt-Ergo and CVC4. All the original contents on this site are protected by the `MIT License <http://opensource.org/licenses/MIT>`_.

Contents
======================

.. toctree::
   :maxdepth: 2

   cvc4
   altergo
   smtv2
   test
   result
   ref

Members
================

    :Hanwen Wu: |HW|    
    :Homepage: http://steinwaywu.info/
    :Email: steinwaywhw AT gmail DOT com

    :Wenxin Feng: |WF| 
    :Homepage: http://cs-people.bu.edu/wenxinf/
    :Email: wenxinf AT bu DOT edu


    .. |HW| image:: images/hanwen_wu.jpg 
            :height: 100px
            :width: 100px
            :align: middle

    .. |WF| image:: images/wenxin_feng.jpg
            :height: 100px                
            :width: 100px                 
            :align: middle

Milestones
=======================

This is a tracking table for the whole lifecycle. It is subject to change according to the actual situation.

    +--------+---------------------------------------------------------------+--------------+--------------+
    | Ticket | Task                                                          | Status       | Assign       |
    +========+===============================================================+==============+==============+
    |1       |  Collecting papers/reports/documentations for these projects  | Finished     | Hanwen/Wenxin|
    +--------+---------------------------------------------------------------+--------------+--------------+
    |2       |  Investigating SMTLIB v2.0, CVC4, Alt-Ergo input languages    | Finished     | Wenxin/Hanwen|
    +--------+---------------------------------------------------------------+--------------+--------------+
    |3       |  Investigating abstract syntax for those input language       | Finished     | Hanwen/Wenxin|
    |        |  within the bit-vectors and integer theories                  |              |              |  
    +--------+---------------------------------------------------------------+--------------+--------------+
    |4       |  Testing Alt-Ergo using SMTLIB v2.0                           | Finished     | Hanwen       |  
    +--------+---------------------------------------------------------------+--------------+--------------+
    |5       |  Testing CVC4 using SMTLIB v2.0                               | Finished     | Wenxin       |
    +--------+---------------------------------------------------------------+--------------+--------------+
    |6       |  Testing Data Analysis                                        | Finished     | Wenxin/Hanwen|
    +--------+---------------------------------------------------------------+--------------+--------------+
    |7       |  Implementing CVC4 & Alt-Ergo front end                       | Finished     | Hanwen/Wenxin|
    +--------+---------------------------------------------------------------+--------------+--------------+