SLIDE: Separation Logic with Inductive Definitions
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F14%3APR27632" target="_blank" >RIV/00216305:26230/14:PR27632 - isvavai.cz</a>
Výsledek na webu
<a href="http://www.fit.vutbr.cz/research/prod/index.php?id=373" target="_blank" >http://www.fit.vutbr.cz/research/prod/index.php?id=373</a>
DOI - Digital Object Identifier
—
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
SLIDE: Separation Logic with Inductive Definitions
Popis výsledku v původním jazyce
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ázev v anglickém jazyce
SLIDE: Separation Logic with Inductive Definitions
Popis výsledku anglicky
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.
Klasifikace
Druh
R - Software
CEP obor
JC - Počítačový hardware a software
OECD FORD obor
—
Návaznosti výsledku
Projekt
Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach
Ostatní
Rok uplatnění
2014
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Interní identifikační kód produktu
SLIDE
Technické parametry
Volně šiřitelný software poskytovaný pod licencí GNU GPL (přesné znění licence je dostupné na stránce http://www.gnu.org/licenses/gpl.html (http://www.gnu.org/licenses/gpl.html)).
Ekonomické parametry
Software je volně dostupný včetně zdrojových textů.
IČO vlastníka výsledku
00216305
Název vlastníka
Vysoké učení technické v Brně