❓When should I use Crux?

Crux tends to work well with small, critical segments of code that primarily perform computation, rather than interacting with the outside world. For example, it is well-suited to code such as cryptographic algorithms, network packet serialization, signal processing, and similar domains. When using Crux to ensure the absence of specific bugs, the code being analyzed should operate only over fixed-size data structures, and include only loops that will terminate after a bounded number of iterations, regardless of the contents of input data. However, Crux can still be useful for finding bugs in programs that operate over unbounded data or use unbounded loops.

For larger programs, or programs where certain portions of code are missing, the Software Analysis Workbench (SAW) allows additional user input to divide programs into components and reason about those components more efficiently by considering them independently.