I have been following the course Concrete Semantics with Isabelle/HOL. At some point we are given the task to verify a program/extend some semantic construction/prove some mathematical fact. I personally prefer to dive a little bit more into operational semantics, so adding new features to the IMP language is the way to go.
The classical extensions are non-determinism/parallel execution. These are described in a variety of books (Winskel, Hennessy or Nielson to cite only classical authors). However, I feel the treatment is rather limited and I'm not sure that can be turned into project, it looks more like a bunch of exercises.
So my question is are you aware of any simple but interesting extensions of the operational semantics approach to the study of a simple WHILE-program (such as IMP)? I would be looking specially for significant properties that can be proved in that semantics and illustrative examples that may be relevant.