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 email@example.com