Safely Detecting Cats with Crux: A Tutorial

A while back, we announced that we were open-sourcing Crux, a software verification tool. I’d like to work through a slightly more involved example in this post than those presented in the original announcement. In particular, I’d like to give an example of how one might apply Crux to verify functional properties of a system […]

Read More

Under-Constrained Symbolic Execution with Crucible

UC-Crux is an open-source command-line tool and Haskell library for performing under-constrained symbolic execution on LLVM code for the sake of exposing bugs or verifying the absence of certain types of undefined behavior. It requires only LLVM bitcode as input. It is built on Galois’s Crucible library for symbolic execution. Under-constrained symbolic execution (developed by […]

Read More

Demo: Symbolic Testing of Rust using Crux

The standard development tools for the Rust language provide a convenient mechanism for embedding tests within your code that can then be automatically run using the `cargo test` command. This video shows how to migrate from testing to verification of Rust programs by converting a standard Rust test to use Galois’ Crux tool. Crux can […]

Read More