SeaHorn

Repositories

• sea-dsa

  A new context, field, and array-sensitive heap analysis for LLVM bitcode based on DSA.

  llvm static-analysis verification pointer-analysis
  C++ 20 79 8 2 Updated Oct 22, 2020

• seahorn

  SeaHorn Verification Framework

  llvm static-analysis verification model-checking program-analysis abstract-interpretation horn-clauses
  C 90 253 6 (1 issue needs help) 5 Updated Oct 22, 2020

• llvm-seahorn

  LLVM components that are modified for SeaHorn

  optimization llvm
  C++ 8 5 0 1 Updated Oct 19, 2020

• crab-llvm

  Static Analyzer for LLVM bitcode based on Abstract Interpretation

  llvm static-analysis program-analysis invariants software-verification abstract-interpretation
  C Apache-2.0 20 135 2 1 Updated Oct 19, 2020

• crab

  CoRnucopia of ABstractions: a language-agnostic library for abstract interpretation

  static-analysis program-analysis abstract-interpretation invariant-generation
  C++ 15 90 14 (1 issue needs help) 0 Updated Sep 21, 2020

• seahorn.github.io

  github-pages repository
  JavaScript 3 0 0 0 Updated Jul 17, 2020

• seahorn-tutorial

  Supplementary files for SSFT 2015 summer school
  LLVM 0 5 0 0 Updated Sep 5, 2019

• sea-cut

  C/C++ refactoring tool for library abstractions

  refactoring c cplusplus static-analysis program-verification
  C++ MIT 0 1 0 0 Updated Aug 23, 2019

• llvm-dsa

  LLVM DSA fork for SeaHorn

  llvm pointer-analysis
  C++ 6 13 0 0 Updated Aug 17, 2019

• seahorn-ext-deps

  Binaries for external dependencies needed to build/use SeaHorn
  MIT 0 2 0 0 Updated Jul 28, 2019

• elina

  Apron Library together with an old version of ELINA (The ETH LIbrary for Numerical Analysis)

  static-analysis abstract-interpretation numerical-domain
  C LGPL-2.1 2 1 1 0 Updated Jul 18, 2018

• ldd

  Library for Decision Diagrams over Linear Arithmetic

  static-analysis abstract-interpretation numerical-domain
  C 0 3 0 0 Updated Oct 4, 2017

• klee

  Forked from klee/klee

  KLEE Symbolic Virtual Machine
  C++ 466 1 0 0 Updated Sep 17, 2016

• sygspacer

  Syntax based invariant synthesis using Spacer
  Python 0 2 0 0 Updated Aug 30, 2016

• z3

  Forked from Z3Prover/z3

  The Z3 Theorem Prover
  C++ 954 1 0 0 Updated May 24, 2016

• seatooling

  Examples of using clang-libtooling
  CMake 1 1 0 0 Updated Apr 11, 2016

• seahorn-doc

  Documentations and tutorial for SeaHorn
  0 0 0 0 Updated Mar 3, 2016

• benchexec

  Forked from sosy-lab/benchexec

  BenchExec: A Framework for Reliable Benchmarking and Resource Measurement
  HTML Apache-2.0 114 0 0 0 Updated Jan 14, 2016

• sv-benchmarks

  Forked from sosy-lab/sv-benchmarks

  SVCOMP 2015 with some tweaks to fix undefined behavior
  C 157 0 0 0 Updated Dec 14, 2015

• clang

  Forked from llvm-mirror/clang

  Mirror of official clang git repository located at http://llvm.org/git/clang. Updated every five minutes.
  C++ 1,598 1 0 0 Updated Dec 12, 2015