Home

Welcome to the bil-to-boogie-translator wiki!

Architecture Overview of the Translator

• Parser
• Analysis phases (including verification conditions)
• Boogie code generation

TODO List

• review intermediate representation (State data structure)
• cleanup generation of memory accesses
  • separate stack from heap (more reliably)
• start with simple boolean security levels
• etc?

Future Ideas

• infer loop invariants