[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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:

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