Grackle is a symbolic execution tool designed for symbolically executing MATLAB ® and LLVM ® code, and evaluating those expressions using SAT and SMT solvers such as ABC and Yices. Grackle is intended to enable engineers to reason symbolically about numerical programs. It can be used to, for example, find inputs that may crash a system or exceeds physical tolerances, model compression and decompression routines, or integrate numerical and symbolic solvers.
The Grackle 0.5 public preview is now available to download from the links below.
A new release, Grackle 1.2, is under development and will be available for commercial licensing. Email contact@galois.com for additional information about licensing Grackle.