Product Details
SLIDE: Separation Logic with Inductive Definitions
Created: 2014
Czech title
SLIDE: Separační logika s induktivními definicemi
Type
software
License
required - free
Authors
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS FIT BUT)
Iosif Radu (VERIMAG)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
Iosif Radu (VERIMAG)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
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/
Licence
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 (GA14-11384S)
Reliability and Security in IT (FIT-S-14-2486)
The IT4Innovations Centre of Excellence (ED1.1.00/02.0070)
Verification and Optimization of Computer Systems (FIT-S-12-1)
Reliability and Security in IT (FIT-S-14-2486)
The IT4Innovations Centre of Excellence (ED1.1.00/02.0070)
Verification and Optimization of Computer Systems (FIT-S-12-1)
Research groups
Departments