Symbolic Abstract Contract Synthesis in a Rewriting Framework

María Alpuente, Daniel Pardo, Alicia Villanueva

We propose an automated technique for inferring software contracts from programs that are written in a non-trivial fragment of C, called KernelC, that supports pointer-based struct…