Scope Logic with Local Reasoning and Pre/Post-State Properties

Jianhua Zhao, Xuandong Li

This paper presents an extension to Hoare logic for pointer program verification. Logic formulas with user-defined recursive functions are used to specify properties on the program…