Symbolic Testing for C and Rust

This tutorial will provide an introduction to Crux, Galois' new open source symbolic testing tool. Traditional testing examines only a small set of test vectors, meaning that the assurance it provides is inherently limited. In symbolic testing, we replace concrete inputs by symbolic variables, and then exhaustively validate the test for all possible input values. Symbolic testing is a type of formal verification, but the close connection to traditional testing makes it much easier to deploy than other approaches. A single symbolic test can efficiently cover billions of possible inputs or more, but an existing test suite can often be made symbolic by trivial code changes.