Automatic Function Annotations for Hoare Logic

Danielle Matichuk

In systems verification we are often concerned with multiple, inter-dependent properties that a program must satisfy. To prove that a program satisfies a given property, the correc…