Skip to content

Home

Jump to bottom Edit New page
Herbert Rocha edited this page Dec 20, 2018 · 3 revisions

**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

Project Architecture

Map2Check works by using LLVM pass to instrument bytecode (Backend-Pass), then implements those functions on Backend-Library, finally the frontend works by processing generated files

Add a custom footer
Add a custom sidebar
Clone this wiki locally