# ABC - Automata-Based model Counter for string constraints

### Overview

The Automata Based Counter (ABC) is a string constriant solver and model counter. ABC provides solutions to systems of string constraints in the form of a deterministic finite automaton. In addition ABC produces symbolic representation of the number of strings within a length bound, k, that satisfy a set of constraints. ABC can also output the number of satisfying solutions for a specific provided bound.

### Source

ABC source code is available on GitHub

### Experimental Data

String, integer, and mixed constraint data

### CAV'15 Experimental Data

We validated ABC on several sets of benchmarks. The counting results and input files are available for download.Java Benchmarks (Original Data Source)

JavaScript Benchmarks (Original Data Source)

Satisfiability Checking (Original Data Source)