Symbol	Meaning
:clock9:	Ongoing implementation
:heavy_check_mark:	Implemented
:x:	Do not implement

Name	Status
Budget example	:clock9: Ongoing implementation
Network session example	:clock9: Ongoing implementation
Sortedness property	:clock9: Ongoing implementation
List summation	:clock9: Ongoing implementation
N-queens	:clock9: Ongoing implementation
Red-black tree	:clock9: Ongoing implementation
Tower of Hanoi solver	:clock9: Ongoing implementation

Example ideas for program repair

Budget example

COLA adjustment example from this paper. There is a redundant field in the data structure that exists to express another "view" into the data (looking at it in terms of weeks vs days).

Network session example

From this paper. A new, redundant, field is added to a data structure to improve efficiency.

Sortedness property

Convert to and from a sorted data structure (for example, a sorted list or a binary search tree) to an unsorted data structure (for example, a stack). Assume sortedness. The program should break when using the unsorted data structure. Next, find a way to patch the program automatically.

Note: This potential limitation is relevant here.

List summation

Folds, such as a summation of a list, seem difficult to express in Suslik currently. These could be of major importance when considering fusion and deforestation, as examples where these techniques are useful often involve folds (and unfolds).

Consider this example, which currently fails to synthesize:

predicate ListSum(loc x, int sum, set vals)
{
| x == 0 => { sum == 0 ; emp }
| not (x == 0) => { vals =i {v} + vals1 && sum == v+acc ; [x,2] ** x :-> v ** (x+1) :-> nxt ** ListSum(nxt, acc, vals1) }
}

void calcListSum(loc x, loc y)
  { x :-> p ** y :-> 0 ** list(p, vals) }
  { x :-> q ** y :-> acc ** ListSum(z, sum, vals) }
{
  ??
}

N-queens problem

This is a classic example of backtracking. Can Suslik synthesize a backtracking algorithm? Also, would it be worth it to have some kind of general-purpose backtracking abstraction, to use for solving backtracking problems?

Red-black tree

Tower of Hanoi solver