University of Utah
School of Computing


MPEC checks for Itanium ording violations automatically. If it is satisfiable, MPEC give out an explantion trace. If unsatisfiable, it extracts an unsat core and displays it as a cyclic graph. It needs Ocaml 3.04 or higher and g++ to be compiled. Besides, it uses zChaff as SAT solver and uses GraphViz to visualize cyclic graph.

Source code can be downloaded here[.tar.gz file].

Itanium specification in HOL

Itanium specified using an Operational Semantics (our ICCD 2001 paper)
back to UV home

School of Computing • 50 S. Central Campus Dr. Rm. 3190 • Salt Lake City, UT 84112
801-581-8224 • Send comments to

Home People Research Admissions Site Map