Automatic refinement-checking of CSP processes with infinite state-spaces

[Allan McInnes <amcinnes@xxxxxxxxxx>]

Hi all,

Just came a cross an interesting paper out of UC San Diego, in which the authors
claim to have developed a method for fully-automated (trace) refinement checking
of CSP processes having infinite state-spaces. Their technique seems to involves
using a combination of state-exploration and automated theorem-proving, and they
claim that the resulting tool does not require human interaction to complete
refinement checks.

I haven't had a chance to read the paper in depth yet. But from a quick skim it
looks fairly promising. Note however that, as far as I can tell, it's only been
published as an internal technical report so far. Still, I thought the folks on
this mailing list might be interested in taking a look at it. You can find the
paper here:
http://www.cs.ucsd.edu/Dienst/UI/2.0/Describe/ncstrl.ucsd_cse/CS2007-0882

Cheers,
Allan
-- 
Allan McInnes <amcinnes@xxxxxxxxxx>
PhD Candidate
Dept. of Electrical and Computer Engineering
Utah State University