| |
| 2.
MPEC -- a memory-ordering checker for Itanium memory model
[.tar.gz file ]
|
|
MPEC is an Itanium memory model checker. It can accept
execution snapshots of multi-threaded program and check whether
they conform Itanium memory model or not. MPEC is written
in a mixture of Ocaml and C++.
|
| |
| 1. Ocaml interface for zChaff
[.tar.gz file] |
|
zChaff is a state-of-art sat solver developed in Princeton
University. With this interface, we can use zChaff in Ocaml, even in the
interactive toplevel. zChaff.2004.11.15 is used here. Please visit
www.princeton.edu/~chaff/
to download zChaff.
|
| |
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Last modification: April 10th, 2005
|
