[fsantanna]

Some colleagues are working on an operational semantics of the language (based on the one in the thesis). This will allow us to prove some claims (e.g., reaction termination, bounded memory). Then, we may think about something else. Anything more specific in mind?

[pron]

Temporal logic verification (via model checking, static analysis, test generation, runtime checks etc.)?

[fsantanna]

That would be interesting.

It seems to be feasible given the language semantics.

We'll definitely investigate it.