ABC - Automata-Based model Counter for string constraints


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.


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)