 |
|
|
||
|
|
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 yuyang@cs.utah.edu
Disclaimer