• Cerberus BMC
    C11 International Standard (N1570 draft)
    REMS
  • File
    New empty file
    Load from file
    CAV 2019
  • Model
    C11
    RC11 (hardcoded)
    RC11
    Linux
    Linux (no RCU)
    Custom herd file
  • Views
    C abstract syntax (Cabs)
    C abstract syntax, typed and desugared (Ail_AST)
    C abstract syntax, typed and desugared (Ail)
    Core
  • Model Checker
  • Compile
  • Options
    Basic rewrites
    Sequentialise operations
    Colour elaboration expression
    Colour every elaboration expression