Cerberus C semantics & pointer provenance

Add to your list(s) Download to your calendar using vCal

• Kayvan Memarian (University of Cambridge)
• Friday 28 February 2020, 13:00-14:00
• Computer Laboratory, room SS03.

If you have a question about this talk, please contact Jean Pichon-Pharabod.

The C programming language is notionally defined by an ISO standard, the “de facto” usage of the language has however diverged over time from the standard semantics. The main point of disagreement concerns the memory object model, and in particular the semantics of pointers. While system programmers often rely on a very concrete view of pointers (sometimes even more concrete than what the ISO standard describes), compiler implementers take a more abstract view. Some compiler optimisations, in particular the ones based on alias analysis, reason about how pointer values are constructed during the program execution instead of only considering their representation.

In this talk, I will present a source-language semantics for pointer values and memory operations formalising a notion of provenance. It aims at reconciling the concrete and abstract views of the C memory model.

This work is part of the Cerberus project, an executable semantics for a substantial fragment of C, which I will also present. In this model, we define the semantics of C by elaboration into a Core intermediate language where we make much of the language subtleties syntactically explicit, while at the same time keeping some level of implementation agnosticism. Being executable, Cerberus can be used as an oracle for exploring the range of behaviours that one should expect for reasonably sized programs.

More information, including a link to Cerberus’ web interface, is available at https://www.cl.cam.ac.uk/~pes20/cerberus

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory, room SS03
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.