Home

Documentation

• CrabIR: Crab Intermediate Representation

• Concrete Semantics for CrabIR

• Crab Architecture

• Available Abstract Domains

• Abstractions for Memory Regions

Licenses

• Some files (those components originally from Ikos) have a NOSA license. These files with NOSA license has a header mentioning the conditions of the license so they are easy to identify.

• These two files here are licensed by

MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson

• The rest of files have Apache 2.0 license.

Crab can optionally download some external packages such as Apron, Elina, Boxes but they are not considered part of Crab codebase. Finally, Crab uses GMP but GMP is not part either of the Crab codebase.

How-To

• How-to add a new abstract domain
• How-to use C++ API to write a CrabIR program and run analysis

Reading

• All Patrick Cousot's publications
• A great tutorial about Abstract Interpretation by A. Mine
• List of papers explaining the theory behind Crab implementation