Advanced Memory and Shape Analyses

One of the main features of C is manual management of memory, which explains the domination of C in systems and performance-critical code. The downside of manual memory management is that designing data structures requires reasoning about custom memory invariants, and that any mistake may lead to severe cybersecurity vulnerabilities. In this chapter, we present two Frama-C plug-ins, the CodexCodex and RMARMA plug-ins, respectively based on physical refinement types and separation logic, that help verify properties of C programs manipulating data structures in memory with minimal guidance from the user.