Commit a2b73ebe authored by Mihaela SIGHIREANU's avatar Mihaela SIGHIREANU
Browse files

some TODO

parent 742a846a
* Notes TODO
** TABLEAUX 21 version
- [ ] update benchmark to have better test of scalability
** Future work
- for journal version: adde flags
+ see summary of loops with flatable behaviour
- with free-lists
** ATVA 21 version
- [X] 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
- [X] 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
- [X] fix Abs+ for v < 2
- [X] see lower bound for complexity of entailment
- [X] experimental results : add benchmark to test scalability
+ ZW is discussion with Loc which is contact with Infer's people
collaborate on solvers? on SL-COMP? on cyclic proofs?
** CADE-28 rebuttal
*** Non linear pointer arithmetic
+ ex p + i*j for array access
+ ex p + 1 << i for binary memory allocator
+ ex p & FFFF << i
+ some of them are modulo contraints
+ what are other cases (see paper given in the review)
+ Q: PA with bit vectors is decidable ?!
*** Complexity of entailment
- is EXPTIME upperbound
- [ ] is coNP-hard ? not sure !
- [X] is coNP-hard
*** Extensions
- with flag (see previous versions)
......
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