Z3JavaScript - Native Z3 Bindings for Node.js


Before we can symbolically execute JavaScript we need a way to invoke an SMT solver directly from JavaScript, however we found that there is almost no existing language support for Node.js. To remedy this we developed Z3JavaScript, an NPM-installable set of bindings to the popular SMT solver Z3. In addition to a set of primitive bindings we provide a set of wrapper classes to simplify usage from JavaScript. We also provide a regular expression rewriter which allows for reasoning about regular expressions, capture groups, and backreferences in programs.