bannera

Book A.
Introduction

Book B.
7150 Requirements Guidance

Book C.
Topics

Tools,
References, & Terms

SPAN
(NASA Only)

Tool title

Title of page above

Type

Open Source

Owner/Source

NASA Ames RSE Group

Link

http://seahorn.github.io

Description

A fully automated analysis framework for LLVM-based languages. Takes an LLVM based program (e.g., C) input program and generates LLVM IR bitcode. Specifically, it performs the pre-processing and optimization of the bitcode for verification purposes. Takes as input the optimized LLVM bitcode and emits verification condition as Constrained Horn Clauses (CHC). The middle-end is in charge of selecting encoding of the VCs and the degree of precision. Takes CHC as input and outputs the result of the analysis. In principle, any verification engine that digests CHC clauses could be used to discharge the VCs. Currently, SeaHorn employs several SMT-based model checking engines based on PDR/IC3. Complementary, SeaHorn uses the abstract interpretation-based analyzer CRAB (A language-agnostic framework for abstract interpretation) for providing numerical invariants.

User

ARC

SWE

SWE-060


  • No labels