Commit 3af7f81b authored by Mihaela SIGHIREANU's avatar Mihaela SIGHIREANU
Browse files

TODO file added

parent 3f000250
* Notes TODO
** TABLEAUX 21 version
- [ ] update benchmark to have better test of scalability
- [ ] change overview to give more insights on the DP
- [ ] improve section 5
- [ ] remove proof of Lemma 2 and introduce definition of Abs
- [ ] composition lemma may be extended to max
- [ ] fix Abs+ for v < 2
- [ ] see lower bound for complexity of entailment
** CADE-28 rebuttal
*** Complexity of entailment
- is EXPTIME upperbound
- [ ] is coNP-hard ? not sure !
*** Extensions
- with flag (see previous versions)
- with free-list on top of heap-list or alone)
- with heap binary tree
- with data about memory allocators
- fragments in VST https://vst.cs.princeton.edu/
** ESOP 21
- [X] article: fix problems in specifications of search/split/join
- [ ] article: use join in a loop for defragmentation to obtain interesting entailment
- [X] article: rewrite overview with the running example of defragmentation
- [X] tool: generate examples for the benchmark from the code (using verifast or VCC) send file to ZW
- [X] tool: improve entail when hck is inlined
- [X] tool: provide entail bench by generating them randomly
- [X] see results of examples
- [ ] generate bench with static arg sz
- [X] article: read and fix problems
- [ ] see extension to dl-hls in order to deal with early coalescing/join
- [X] simplify hck with only one field (size) to simplify dp for entailment
- [ ] use UF to represent size and status
- [ ] fragment with pto, blk and hck is reducible to pto and blk using UF ?
** Skype 02/17/2020
- consider fragment of blk/fck with list ID using it
** Beijin 09/2018
- abstraction of heap allocation using blk in ASL
- introduce relation with fsx(x) in the summary
* Biblio
** Kimura & Tatsuta : DECIDABILITY FOR ENTAILMENTS OF SYMBOLIC HEAPS WITH ARRAYS
- https://arxiv.org/abs/1802.05935
- combines ls and dll with block (array) but block not inside ID
- propose a sound set of proof rules and then proof the set is complete
** Navarro Perez & Rybalchenko : Separation logic + superposition calculus = heap theorem prover
- PLDI 2011
- reduction to reasoning about equality
** James Brotherston and Max Kanovich : On the Complexity of Pointer Arithmetic in Separation Logic
- no polynomial algorithm is pointer arithmetics introduced
in SL (without ID)
- APLAS 2016
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment