Automating Model Checking Cache Coherence with Memory Consistency

Summary: Verifying that a cache coherence protocol (CCP) adheres to the memory consistency model (MCM) in concurrent programming is of vital importance. Various manual approaches have been attempted (through proofs, simulation, testing) in the past. Each of these had the downfall of being tailored to a specific protocol/model pair. I have developed a direct model […]

Continue reading

Medications at what cost?

Timed Automata (TA), first introduced by Alur and Dill [1], is now a standard modeling formalism for describing the behaviour of real-time systems. Several mature automated model checking tools exist (e.g. Kronos, Uppaal) and have been applied to the quantitative analysis of numerous industrial case-studies. Priced Timed Automata (PricedTA) [2] extend timed automata with further […]

Continue reading