Research interest

Formal Verification

Formal verification uses mathematical models and precise specifications to reason about whether a system behaves as intended. It is particularly valuable for concurrent software, where different orders of execution can create behaviours that are difficult to examine through conventional testing alone.

Dr. Alshammari’s work in this area focuses on runtime verification and Interval Temporal Logic. His publications on channels and shunts examine how a parallel runtime verification framework can handle synchronous and asynchronous message passing. These studies connect the specification of correctness properties with the observation of systems during execution.