Simon Wimmer

Typically, Turing machines allow the head to not be moved at all when taking a transition. This change adds such a 'neutral' movement, with the designated letter 'N'.

The UPPAAL bytecode seems to support a `STORE` instruction, which puts a value into a register but specifies both arguments **on the stack**. This is problematic because it interferes with...

`CALL` & `RETURN` are not supported at the moment because we do not have a clue of where they will continue the program execution. Reasons: - The current program reachability...

To improve memory consumption, symbolic states can be shared between the passed & wait list. This requires a low-level verification of the corresponding data structure.

To correctly analyze local clock ceilings, we need to identify the set of clocks that are **always** reset on a certain edge. The current program analysis for this property is...

Instructions that could get stuck in case there are not enough elements on the stack are not supported at the moment. In principle, this should not be a problem since...