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

New BSD-Licensed SAW Release

A new release of the Software Analysis Workbench (SAW) is now available! This release includes a large collection of new features and bug fixes enabling verification of a wider variety of Java and LLVM programs. A list of changes is available here, along with binaries for a variety of platforms. Additionally, this release changes the […]

Read More

Announcing the Software Analysis Workbench

We are pleased to announce a public preview of the Software Analysis Workbench. The Software Analysis Workbench (SAW) provides the ability to formally verify properties of code written in C, Java, and Cryptol. It leverages automated SAT and SMT solvers to make this process as automated as possible, and provides a scripting language, called SAW […]

Read More