HORSC (HORS plus case)

We have created a novel type system that characterises the universal model-checking problem for HORSC against deterministic trivial tree-automata. For now, the web interfaces are available at:

• Model check HORSC directly
• Perform abstraction of PMRS first

The long form of our ICFP 2012 paper is also available here.