Soteria Documentation

Soteria is a comprehensive library for writing symbolic execution engines. The library is parametric and allows for defining one's own notion of symbolic value or solver, enabling arbitrary language-specific optimisations. Our goal is for symbolic execution engines to be easy to write, easy to read, highly customisable and efficient.

Manual contents

• The symbolic execution tutorial walks you through the basics of doing symbolic execution with Soteria.
• The logging tutorial explains how to use the Logs module for debugging and monitoring your analyses.
• The statistics tutorial shows how to track and report metrics during symbolic execution.
• The sym_state PPX tutorial explains how to derive symbolic state boilerplate.

Library

Core components of Soteria, enabling symbolic execution, solver-interaction, user-friendly reporting, and more.

• Soteria.Symex The core of Soteria symbolic execution.
• Soteria.Data Symbolic abstractions over common data structures.
• Soteria.Sym_states Separation-logic ready state modules.
• Soteria.Logic Separation logic assertions
• Soteria.Solvers Low-level solver manipulation and utilities.
• Soteria.Logs Logging facilities for symbolic execution.
• Soteria.Terminal Utilities for displaying messages to the user.
• Soteria.Stats Tracking of statistics across symbolic execution.
• Soteria.Config Global configuration module.
• Soteria.Smt Performance-focused SMT-LIB s-expression and solver interface.
• Soteria.Soteria_std Standard library extensions and utilities for Soteria.

The two built-in symbolic value implementations, to get started; you can also define your own!

• Soteria.Tiny_values Minimal natural integer based values. Suitable for toy examples.
• Soteria.Bv_values Extensible bit-vector based values, with floating point support. Suitable for low-level languages.