Automatic Verification Based on Abstract Interpretation

This paper reconstructs and extends the automatic verification technique of Le Metayer, Proving properties of programs defined over recursive data structures (ACM PEPM ’95), based on a backward abstract interpretation. To show the effectiveness of extensions, we show two examples of the declarative specifications of sorting and formatting programs, which are directly and concisely expressed in our specification language