Tool title |
Title of page above |
Type |
Open Source |
Owner/Source |
NASA Ames RSE Group |
Link |
|
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 |
