Soteria is a comprehensive library for writing symbolic execution engines. The library is very 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.
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 assertionsSoteria.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.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 Bit-vector based values, with floating point support. Suitable for low-level languages.