Kaluza String Solver

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.

A binary release for Ubuntu 9.10 is available here.
The (50,000+) test cases available below were generated as part of our analysis using Kudzu our symbolic execution framework for Javascript. All the test cases are obtained from lowering JavaScript operations from real-world AJAX web applications.

Satisfiable Cases   Unsatisfiable Cases
Input Language
The input language for Kaluza is here.
Related Links