Talk Keyword Index

TALK KEYWORD INDEX

This page contains an index consisting of author-provided keywords.

Shortcuts: B C D E F G I L M P R S T U V

B
benchmarks	Report on SL-COMP
Bunched Logic	Labelled Tableaux for Linear Time Bunched Implication Logic
C
Concurrent Separation Logic	Proving Logical Atomicity using Lock Invariants Functional correctness specifications for concurrent data structures: Logical Atomicity in Iris
D
Data Structures	Deciding Separation Logic with Heap Lists
decision procedure	Deciding Separation Logic with Heap Lists
E
Entailment problem	Two Results on Separation Logic With Theory Reasoning
expressiveness	On the Expressiveness of a Logic of Separated Relations
F
fine-grained locking	Proving Logical Atomicity using Lock Invariants
G
Garbage Collection	Polishing a Rough Diamond: An Enhanced Separation Logic for Heap Space under Garbage Collection
I
Inductive reasoning	Two Results on Separation Logic With Theory Reasoning
Iris	Proving Logical Atomicity using Lock Invariants Functional correctness specifications for concurrent data structures: Logical Atomicity in Iris
L
Labelled Tableaux	Labelled Tableaux for Linear Time Bunched Implication Logic
Linear Time Logic	Labelled Tableaux for Linear Time Bunched Implication Logic
logical atomicity	Proving Logical Atomicity using Lock Invariants Functional correctness specifications for concurrent data structures: Logical Atomicity in Iris
M
Memory allocation	Deciding Separation Logic with Heap Lists
model theory	On the Expressiveness of a Logic of Separated Relations
P
Program Verification	Polishing a Rough Diamond: An Enhanced Separation Logic for Heap Space under Garbage Collection
R
Resource Semantics	Labelled Tableaux for Linear Time Bunched Implication Logic
S
separated relations	On the Expressiveness of a Logic of Separated Relations
Separation Logic	Polishing a Rough Diamond: An Enhanced Separation Logic for Heap Space under Garbage Collection Deciding Separation Logic with Heap Lists Two Results on Separation Logic With Theory Reasoning Report on SL-COMP
Solver Competition	Report on SL-COMP
T
TBA1	Exact Separation Logic
TBA2	Exact Separation Logic
TBA3	Exact Separation Logic
U
Undecidability	Two Results on Separation Logic With Theory Reasoning
V
Verified Software Toolchain	Proving Logical Atomicity using Lock Invariants