munta
munta copied to clipboard
wimmers
Fully verified model checker for realtime systems
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...