Microverification security of modern computing systems with relaxed memory behavior