The CORE system: Animation and functional correctness of pointer programs

E. Maclean, A. Ireland, G. Grov

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Pointers are a powerful and widely used programming mechanism, but developing and maintaining correct pointer programs is notoriously hard. Here we describe the CORE1 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.
Original languageEnglish
Title of host publicationAutomated Software Engineering (ASE), 2011 26th IEEE/ACM International Conference on
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Pages588-591
Number of pages4
ISBN (Print)978-1-4577-1638-6
DOIs
Publication statusPublished - 1 Nov 2011

Keywords

  • computer animation
  • formal verification
  • planning (artificial intelligence)
  • program debugging
  • program diagnostics
  • theorem proving
  • CORE functional correctness capability
  • CORE system
  • IsaPlanner proof planner
  • Smallfoot
  • data structure animation
  • formal guarantees
  • formal proof
  • functional invariants
  • planning subsystem
  • pointer programs
  • reasoning tools
  • shape analysis
  • static analysers
  • term synthesis
  • Animation
  • Cognition
  • Computer science
  • Data structures
  • Educational institutions
  • Planning
  • Shape
  • animation
  • automatic verification
  • proof planning
  • separation logic

Fingerprint

Dive into the research topics of 'The CORE system: Animation and functional correctness of pointer programs'. Together they form a unique fingerprint.

Cite this