Result Details

SLIDE: Separation Logic with Inductive Definitions

Created: 2014
Type
software
Language
English
Authors
Rogalewicz Adam, doc. Mgr., Ph.D., DITS (FIT)
Radu Iosif
Vojnar Tomáš, prof. Ing., Ph.D., DITS (FIT)
Description

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.
Keywords

Separation logic, inductive definitions, entailment

Location

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

License
In order to use the result by another entity, it is always necessary to acquire a license
License Fee
The licensor does not require a license fee for the result
License Conditions

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

Projects
Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures, GACR, Standardní projekty, GA14-11384S, start: 2014-01-01, end: 2016-12-31, completed
Centrum excelence IT4Innovations, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, start: 2011-01-01, end: 2015-12-31, completed
Spolehlivost a bezpečnost v IT, BUT, Vnitřní projekty VUT, FIT-S-14-2486, start: 2014-01-01, end: 2016-12-31, completed
Verifikace a optimalizace počítačových systémů, BUT, Vnitřní projekty VUT, FIT-S-12-1, start: 2012-01-01, end: 2014-12-31, completed
Research groups
Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)
Departments
Department of Intelligent Systems (DITS)
Back to top