University of Utah
Search
School of Computing

MPEC

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

Home People Research Admissions Site Map