Overview
An attempt at utilizing Maude for formally verifying concurrent system properties such as consistency and safety guarantees by analyzing the HotelReservation component of the DeathStar Microservice benchmark.

Useful Resources
More information on Maude as a Rewrite Logics Implementation and a formal verification tool, please refer to The Maude System.
Special thanks to Professor José Meseguer for all the guidance and teaching along the way.