Discover is a static anlaysis and formal verification framework for computer software with many great features including:
Discover is a static analysis and formal verification tool that can automatically find security bugs and vulnerabilities in programs written in both general-purpose programming languages, such as C, C++, Go, and domain-specific languages, like Solidity (for writing smart contract).
Memory Leaks, Null Pointer Dereference, Buffer Overflow, etc.
Integer Overflow, Integer Underflow, Division by Zero, etc.
Reentrancy, Out of Gas, etc.
Discover is developed using the OCaml programming language. It includes two main parts.
We have provided a detailed documentation as well as specific code examples to help new users get started. Feel free to contact us if you have any query regarding the use of Discover.