SLIDE: Separation Logic with Inductive Definitions

SLIDE: Separační logika s induktivními definicemi

software

In order to use the result by another entity, it is always necessary to acquire a license

The licensor does not require a license fee for the result

Rogalewicz Adam, doc. Mgr., Ph.D. (DITS)
Radu Iosif
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)

Separation logic, inductive definitions, entailment

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.

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

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

Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures, GACR, Standardní projekty, GA14-11384S, 2014-2016, completed
Spolehlivost a bezpečnost v IT, BUT, Vnitřní projekty VUT, FIT-S-14-2486, 2014-2016, completed
The IT4Innovations Centre of Excellence, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, 2011-2015, completed
Verifikace a optimalizace počítačových systémů, BUT, Vnitřní projekty VUT, FIT-S-12-1, 2012-2014, completed

Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)

Department of Intelligent Systems (DITS)