Software Engineering Institute | Carnegie Mellon University
Software Engineering Institute | Carnegie Mellon University

Digital Library



  • Abstract

    SeaHorn is an automated analysis framework for LLVM-based languages. The key distinguishing feature of SeaHorn is its modular design that separates the concerns of the syntax of the programming language, its operational semantics, and the verification semantics. SeaHorn encompasses several novelties:

    • encodes verification conditions using an efficient yet precise inter-procedural technique
    • provides flexibility in the verification semantics to allow different levels of precision,
    • leverages the state-of-the-art in software model checking and abstract interpretation for verification, and
    • uses Horn-clauses as an intermediate language to represent verification conditions which simplifies interfacing with multiple verification tools based on Horn-clauses

    SeaHorn provides several components that are installed via the extra target. These components can be used by other projects outside of SeaHorn. See the for more details.

Software Information

Published by GitHub

Get the Software