A web interface to Kaluza is now available.
Kaluza is a solver for multiple string variables of bounded length. Kaluza constraints may contain word equations over string variables, membership in regular languages, and inequality formulas over string length. Given an input formula, Kaluza outputs string constants that satisfy all the variables in it, or reports that the formula is unsatisfiable. Kaluza is expressive and efficient, and we have successfully used it for testing and analysis of real-world JavaScript programs.
Kaluza was developed as the core of Kudzu, our JavaScript symbolic execution framework.