Highly Automated Formal Proofs over Memory Usage of Assembly Code

Computer Science

• Assembly Code 100%
• Assembly Instruction 50%
• Case Study 50%
• Control Flow 50%
• Data Structure 50%
• Hypervisor 50%
• Interactive 50%
• Invariant 50%
• Nested Loop 50%
• Postcondition 50%
• Production Code 50%
• Proof 100%
• Return Address 50%
• Security Properties 50%
• Theorem Proving 50%

Keyphrases

• Assembly Code 100%
• Assembly Instructions 33%
• Assembly Programs 66%
• Compositional Reasoning 33%
• Control Flow 33%
• Formal Proof 100%
• Interactive Theorem Proving 33%
• Invariant Control 33%
• Memory Consumption 100%
• Memory Layout 33%
• Memory Regions 33%
• Nested Loops 33%
• Production Code 33%
• Return Address 33%
• Security Properties 33%
• Verification Method 33%
• Xen Hypervisor 33%