Home

Welcome to the Map2Check wiki!

This wiki will try to guide you through some of the project structure and common usages

Map2Check works by transforming the C code into LLVM bytecode and reasoning about this bytecode using transformations to inject custom functions and behaviours. Finally it links this bytecode with a custom C library, then executes this code and checks for the behaviour, generating a test case for invalid programs.

Map2Check has the following features:

• Memory, Reachability, Signed Overflow, Assert verification
• Non-deterministic number generation
• Witness generation
• Test-case generation

Property Analysis

To check these properties, Map2Check transforms and injects into custom functions based on current verification mode:

Memory Analysis

Overflow

Reachability

Assert

Project Architecture

Backend-Library

Backend-Pass

Frontend