Check that the computing alternatives is correct in the presence of programs where transitions disable transitions

Currently, we check if a thread has exited by checking if there are no successors of the current position of the thread. This solution does not work for more complex CFGs. Probably the best solution is to have a boolean variable in the state of a thread that marks whether the thread as already hit the exit/return statement.

Currently, we are computing unconditional independence relations based on read-write sets. Possible extensions include:

• Enrich the read-write set with new information: operations, values, variables.
• Introduce a mode where the independence relation is computed on-the-fly. Is this sound w.r.t to extension function?

In the case of enabledness of the join and mutexes, the implementation was just checking the case where the edge in the CFG was a join and a mutex and making the appropriated changes. However, this is not sufficient because there might be arbitrary local code before such join and mutex lock. There are two options possible:

1. Consider a thread disabled if it was would reach such edge.
2. Generate summaries of events that are not global.

Collapse needs to return the collection of actions and not only the one associated with the last edge of the CFG

Within a configuration, we would like to apply widening even if multiple executions of collapse have been issued. That is the only way to achieve termination of the analysis.
There are two possibilities to implement this feature:

1. In the collapse by passing extra information, e.g. the CFG annotated with the previous states.
2. In the unfolding algorithm, by keeping track per configuration a Map from EventName to IntState.

In preparation for full support of arrays.

Currently, poet is an explicit-state model checker. Modify the execution engine to allow formulas.
This involves a major revision of the current engine:

• Convert the code to SSA on-the-fly.
• State is just a Map Variable Value. This needs to be changed so that State can be a Formula.
• Converter needs to be completely re-written.
• Independence relation computation?
• Reduce the problem of checking which transitions are enabled to a satisfiability problem.

Currently, the front end uses the GCC pre-processor which means that all the code from the includes is incorporated into the model.

Verify that the transformers for arrays are correct.

Threads are enabled whenever:

1. It was created: there is a pc associated to the thread id.
2. It is not in a join statement for an enabled thread: the pc is not a join OR the pc is a join and the thread associated with the join has terminated.
3. It is not in a lock for a lock that is taken: the pc is not a lock OR it is a lock and the lock is free.