ToDo

Jump to bottom Edit New page

Aggelos Giantsios edited this page Aug 24, 2015 · 1 revision

Topics

Strategy

Search strategy to improve coverage.
Search strategy to target specific code.
Investigate ways to deal with path explosion.

Concurrency

Find bugs in non-deterministic concurrent programs.

SMT Solving

Fully support bitstrings, maps, funs, dicts in Z3.
Efficiently encode recursive datatypes in Z3.
Investigate the possibility to use other solvers.
Extend spec language to be able to describe type invariants.

Other

Implement External Term Format with sharing / constant expression elimination.