Prof. Ing. Tomáš Vojnar, Ph.D.

SLIDE: Separation Logic with Inductive Definitions

Authors:Rogalewicz Adam, Iosif Radu, Vojnar Tomáš
Type:software
Created:2014
Licence:required - no fee
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:
The tool is available at: http://www.fit.vutbr.cz/research/groups/verifit/tools/slide/
Research groups:
Departments:
Licence terms:
Free software under the terms of GNU GPL (cf. http://www.gnu.org/licenses/gpl.html).

Your IPv4 address: 54.91.171.137
Switch to IPv6 connection

DNSSEC [dnssec]