Detail aplikovaného výsledku

SLIDE: Separation Logic with Inductive Definitions

ROGALEWICZ, A.; IOSIF, R.; VOJNAR, T.

Originální název

SLIDE: Separation Logic with Inductive Definitions

Anglický název

SLIDE: Separation Logic with Inductive Definitions

Druh

Software

Abstrakt

SLIDE is a prototype tool for checking entailment in Separation Logicwith 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.

Abstrakt aglicky

SLIDE is a prototype tool for checking entailment in Separation Logicwith 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.

Klíčová slova

Separation logic, inductive definitions, entailment

Klíčová slova anglicky

Separation logic, inductive definitions, entailment

Umístění

Nástroj i dokumentaci lze získat na URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/slide/

Licenční poplatek

K využití výsledku jiným subjektem je vždy nutné nabytí licence

www

https://www.fit.vut.cz/research/product/373/