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.

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

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 within the bit-vectors and integer theories Finished Hanwen/Wenxin
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

Project Versions

Table Of Contents

Next topic

CVC4

This Page