CoqCat is a formalization in Coq of axiomatic memory models. These models can already be designed, simulated and tested against real hardware using the tools of the DIY Toolbox.
The goal of this development is to formalize these memory models and to prove interesting properties about them.
To compile the project, run make.
If you want to generate the documentation using coqdoc, run make html.
The author of CoqCat is Jade Alglave.
Copyright 2010 Institut National de Recherche en Informatique et en Automatique. All rights reserved. This file is distributed under the terms of the Lesser GNU General Public License.
