Qodana vs SeaHorn

Qodana analyzes code from the IDE through CI to find code smells, duplication, complexity, vulnerabilities, and license issues. Its baselines mark findings as new, unchanged, or resolved, and quality gates can block CI/CD pipelines based on issue counts, severity, coverage, or vulnerable and license-incompatible dependencies. Taint analysis identifies risks such as SQL injection, cross-site scripting, command injection, and path traversal. Qodana supports most JetBrains IDEs, along with VS Code, Visual Studio, and Cursor. Listed CI integrations include GitHub Actions, GitLab, TeamCity, Jenkins, and Azure Pipelines; Docker images can run in CI/CD pipelines. Self-Hosted runs within an organization’s infrastructure with Docker or Kubernetes deployment options. The Community plan is free and includes one team and 30 days of detailed history. Ultimate costs $5.00 per active contributor per month billed annually at $60.00; Ultimate Plus costs $15.00 per active contributor per month billed annually at $180.00. Licensing uses active contributors over the past 90 days, with a minimum of three.

SeaHorn is a free, open-source framework for automated analysis of C and other LLVM-based programs, developed mainly for research in automated verification. It is not an out-of-the-box static analyzer. Its frontend prepares LLVM IR bitcode, and its middle end converts optimized bitcode into verification conditions written as Constrained Horn Clauses. Backend engines use SMT-based model checking, including PDR/IC3 techniques, and CRAB can provide numerical invariants through abstract interpretation. SeaHorn supports abstract interpretation, context-sensitive pointer analysis, bounded model checking, constrained-Horn-clause software model checking, and termination or non-termination analysis. For C programs with assertions, `sea pf` translates the program, generates and solves verification conditions, displays invariants for safe results, or saves a counterexample for violations. `sea inspect` reports program structure and can produce memory or call-graph data. The framework also checks generated clauses for inconsistent code fragments using path coverage. Docker is described as the easiest starting point, with a nightly image refreshed daily. Building requires LLVM, Z3, and Boost, whose exact versions change. SeaHorn runs on Linux, macOS, or self-hosted systems under a modified BSD license.