Symbolic Execution

Automatically explore the program behaviors and find the inputs leading to a given execution state.

Safety and Security

Instruments the execution with additional assertions and property checks to reveal bugs or security violations.

Binary Code

Analyse programs in executable format, as they are loaded by the operating system and run by the processor.

Instruction Set Architecture

Decoder support for well established Instruction Set Architectures like the x86, ARM or RISCV.