Documents

Learn How to Use SeaHorn

1. Installing SeaHorn: Instructions for SeaHorn installation.
2. SeaHorn tools: Overview of the main tools provided by SeaHorn.
3. SeaHorn options: Overview of the main command-line options used for verification.
4. Writing unit proofs: Instructions for writing verification tasks.
5. SeaBMC: Overview of how verification conditions generated by SeaHorn.

1. Installing SeaHorn

Docker

To get the most recently version of SeaHorn, we provide a Docker container which builds SeaHorn nightly.

Using the following command to pull the nightly built container:

$ docker pull seahorn/seahorn-llvm14:nightly

The dockerfile to build a container locally is provided in the docker folder. The instructions are provided in README.md.

Build SeaHorn Locally

Prerequisites

2. SeaHorn tools

SeaHorn pipeline

3. SeaHorn options

4. the components of a unit proof

Unit proof (proof harness) is a piece of code:

1. Sets the environment for verification (pre-condition)
2. Calls function under verification
3. Validates the result (post-condition)

Intrinsic functions in SeaHorn

To provide the context of specific operations or calculations for verification, SeaHorn offers a collection of built-in functions declared in include/seahorn/seahorn.h including:

Pre- and post-conditions settings

• assume(bool): set a condition to be assumed as "true" by the verifier.

Spatial memory safety checks

Spatial memory safety is xxx.[TODO]

• bool sea_is_dereferenceable(const void *ptr, intptr_t offset):