LogoLogo
Galois Website
SAW
SAW
  • SAW: The Software Analysis Workbench
  • DOCUMENTATION
    • 📋SAW Tutorials and Manual
    • 📚Publications
  • Crux
    • 🔣What is Crux?
    • ❓When should I use Crux?
    • ⬇️Download Crux
  • OPEN SOURCE
    • Overview
    • How to Contribute
  • Download
    • Get SAW
      • Public Key
Powered by GitBook
On this page
Export as PDF
  1. Crux

What is Crux?

PreviousPublicationsNextWhen should I use Crux?

Last updated 3 months ago

Crux is a tool for improving the assurance of software using symbolic testing, currently supporting C/C++ and Rust. Crux can provide you with additional assurance that your code does what you want it to do, and provides higher coverage of possible inputs than techniques such as randomized fuzzing or unit testing.

Specifically, Crux uses symbolic reasoning to check tests exhaustively, on all possible inputs, rather than on a smaller number of fixed or randomly-chosen values. In this way, Crux improves the coverage possible with , a popular approach supported by .

Crux can:

  • Perform symbolic reasoning to evaluate tests exhaustively

  • Analyze C/C++ and Rust code

  • Generate counter-examples when tests fail

  • Generate executable versions of counter-examples to load in a debugger

  • Generate complete models of programs to comprehensively rule out failure cases

Crux is available open-source under the 3-Clause BSD License .

🔣
property-based testing
libraries
for
many
languages
on GitHub