CVC4

An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

About
News
Downloads
Documentation
Publications
Awards
People
History
Third-Party Applications
Acknowledgements

Try CVC4 online!


CI

A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions

Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett, Morgan Deters

This site provides our paper A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions and related material at CAV 2014.

An extended version of our paper at CAV 2014 can be found below.

All materials to reproduce the experimental evaluation in our paper can be found below.

Downloads

Solver Configurations

We have used the following versions in our experiments:

Please note that:

More details are available in the README.txt file in the artifact above.

Results

The compiled results are available as a CSV file, available in the artifact above. For convenience, it also available here. It is documented in the README file above.