software

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      (http://www.fit.vutbr.cz/research/groups/verifit/tools/libvata) tree      automata library.

Separation logic, inductive definitions, entailment

21. 3. 2014

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

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

Poskytovatel licence na výsledek nepožaduje licenční poplatek

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