Verify heaps via unified model checking

This paper addresses the problem of verifying heap evolution properties of pointer programs. To this end, a new unified model checking approach with MSVL (Modeling, Simulation and Verification Language) and PPTL^SL is presented. The former is an executable subset of PTL (Projection Temporal Logic) while the latter is an extension of PPTL (Propositional Projection Temporal Logic) with separation logic. MSVL is used to model pointer programs, and PPTL^SL to specify heap evolution properties. Technically, on one hand, models of MSVL programs are characterized by Normal Form Graphs (NFGs). On the other hand, PPTL^SL is equisatisfiably reduced to its subset which can reuse the decision procedure of PPTL. Our technique is able to deal with a variety of pointer structures such as linked lists and composite structures. In addition, we implement a prototype tool by using an SMT solver as the verification engine in order to demonstrate our approach.