Exit Criteria:

• Developers can relate analysis results with decompiled P-Code or other layers of the Tower of IRs.

Deliverables:

• A tool for aggregating and presenting verification results based on a specified layer of representation.