Product Details

SLIDE: Separation Logic with Inductive Definitions

Created: 2014

Czech title
SLIDE: Separační logika s induktivními definicemi
Type
software
License
required - free
Authors
Keywords

Separation logic, inductive definitions, entailment

Description

SLIDE is a prototype tool for checking entailment in Separation Logic with user-provided inductive definitions of recursive data structures (lists, trees, and beyond) Basic features:

  • Sound and complete for local data structures (doubly-linked lists, trees with parent pointers, etc.)
  • Sound for non-local data structures (trees with linked leaves, skip-lists, etc. )
  • Built on top of the VATA tree automata library.
Location
Licence

Free software under the terms of GNU GPL (cf. http://www.gnu.org/licenses/gpl.html).

Back to top