SeaHorn

All

32 repositories

seaurchin-llvm
Public
The LLVM Project is a collection of modular and reusable compiler and toolchain technologies. This version of LLVM is designed to work with SeaUrchin.
LLVM
•
Other
•15k•0•0•0•Updated Jul 30, 2025Jul 30, 2025
verify-rust
Public
Verify rust programs using seahorn
Jupyter Notebook
•1•1•1•0•Updated Jul 25, 2025Jul 25, 2025
seaurchin
Public
Empowering Rust to build reliable and efficient software.
Rust
•
Other
•14k•1•0•0•Updated Jun 9, 2025Jun 9, 2025
seahorn
Public
SeaHorn Verification Framework
static-analysis model-checking program-analysis abstract-interpretation horn-clauses llvm verification
C
•
Other
•130•455•21•9•Updated May 27, 2025May 27, 2025
crab
Public
A library for building abstract interpretation-based analyses. **Update**: crab is still actively maintained. Please use branch dev.
static-analysis verification program-analysis invariants abstract-interpretation
C++
•
Apache License 2.0
•32•245•6•0•Updated Oct 23, 2024Oct 23, 2024
seamock
Public
SeaMock is a mocking framework for verification
CMake
•
BSD 2-Clause "Simplified" License
•0•1•0•0•Updated Sep 19, 2024Sep 19, 2024
seaurchin-rust
Public
Rust to SEA-IR compiler
MIT License
•0•1•0•0•Updated Jul 13, 2024Jul 13, 2024
sea-dsa
Public
A new context, field, and array-sensitive heap analysis for LLVM bitcode based on DSA.
llvm static-analysis verification pointer-analysis
C++
•
Other
•32•165•10•4•Updated Jun 13, 2024Jun 13, 2024
verify-c-common
Public
C
•14•17•7•5•Updated May 30, 2024May 30, 2024
seahorn.github.io
Public
github-pages repository
JavaScript
•5•0•0•0•Updated May 14, 2024May 14, 2024
clam
Public
Static Analyzer for LLVM bitcode based on Abstract Interpretation. **Update**: clam is still actively maintained. Please use branch dev14.
llvm static-analysis program-analysis invariants software-verification abstract-interpretation
C
•
Apache License 2.0
•41•281•2•1•Updated Apr 21, 2024Apr 21, 2024
crab-pplite
Public
Crab abstract domain wrapper for PPLite domains
C++
•
Other
•0•0•0•0•Updated Apr 9, 2024Apr 9, 2024
verify-mbedtls
Public
Verification jobs for the mbedtls project
BSD 2-Clause "Simplified" License
•0•0•0•0•Updated Oct 3, 2023Oct 3, 2023
ebpf-verifier
Public
A new eBPF verifier, using abstract interpretation
C++
•
MIT License
•48•2•4•2•Updated Aug 18, 2023Aug 18, 2023
llvm-seahorn
Public
LLVM components that are modified for SeaHorn
optimization llvm
C++
•
Other
•7•8•1•1•Updated Aug 11, 2023Aug 11, 2023
verifyTrusty
Public
C
•4•4•2•3•Updated May 26, 2023May 26, 2023
mlir2crab
Public
A MLIR frontend for Crab
C++
•0•0•0•0•Updated Dec 30, 2021Dec 30, 2021
seahorn-tutorial
Public
Supplementary files for SSFT 2015 summer school
LLVM
•
Other
•2•11•0•0•Updated Sep 5, 2019Sep 5, 2019
sea-cut
Public
C/C++ refactoring tool for library abstractions
refactoring c cplusplus static-analysis program-verification
C++
•
MIT License
•0•2•0•0•Updated Aug 23, 2019Aug 23, 2019
llvm-dsa
Public
LLVM DSA fork for SeaHorn
llvm pointer-analysis
C++
•
Other
•8•21•1•0•Updated Aug 17, 2019Aug 17, 2019
seahorn-ext-deps
Public
Binaries for external dependencies needed to build/use SeaHorn
MIT License
•0•2•0•0•Updated Jul 28, 2019Jul 28, 2019
SeaSTL
Public
C++ STL implementation for SeaHorn
C++
•
MIT License
•4•1•0•0•Updated Mar 7, 2019Mar 7, 2019
elina
Public
Apron Library together with an old version of ELINA (The ETH LIbrary for Numerical Analysis)
static-analysis abstract-interpretation numerical-domain
C
•
Other
•2•1•1•0•Updated Jul 18, 2018Jul 18, 2018
ldd
Public
Library for Decision Diagrams over Linear Arithmetic
static-analysis abstract-interpretation numerical-domain
C
•
Other
•1•3•0•0•Updated Oct 4, 2017Oct 4, 2017
klee
Public
KLEE Symbolic Virtual Machine
C++
•
Other
•695•1•0•0•Updated Sep 17, 2016Sep 17, 2016
sygspacer
Public
Syntax based invariant synthesis using Spacer
Python
•
Other
•0•2•0•0•Updated Aug 30, 2016Aug 30, 2016
z3
Public
The Z3 Theorem Prover
C++
•
Other
•1.5k•1•0•0•Updated May 24, 2016May 24, 2016
seatooling
Public
Examples of using clang-libtooling
CMake
•
Other
•2•2•0•0•Updated Apr 11, 2016Apr 11, 2016
seahorn-doc
Public
Documentations and tutorial for SeaHorn
0•0•0•0•Updated Mar 3, 2016Mar 3, 2016
benchexec
Public
BenchExec: A Framework for Reliable Benchmarking and Resource Measurement
HTML
•
Apache License 2.0
•212•1•0•0•Updated Jan 14, 2016Jan 14, 2016