The CORE system: Animation and functional correctness of pointer programs

Pointers are a powerful and widely used programming mechanism, but developing and maintaining correct pointer programs is notoriously hard. Here we describe the CORE¹ system, which supports the development of provably correct pointer programs. The CORE system combines data structure animation with functional correctness. While the animation component allows a programmer to explore and debug their algorithms, the functional correctness component provides a stronger guarantee via formal proof. CORE builds upon two external reasoning tools, i.e. the Smallfoot family of static analysers and the IsaPlanner proof planner. At the heart of the CORE functional correctness capability lies an integration of planning and term synthesis. The planning subsystem bridges the gap between shape analysis, provided by Smallfoot, and functional correctness. Key to this process is the generation of functional invariants, i.e. both loop and frame invariants. We use term synthesis, coupled with IsaPlanner´s capability for reasoning about inductively defined structures, to automate the generation of functional invariants. The formal guarantees constructed by the CORE system take the form of proof tactics.