[erlang-questions] Looking for tricky protocol examples for verification research

Jonathan Schuster schuster@REDACTED
Wed Oct 29 18:36:03 CET 2014


This morning I happened to find the "Erlang and Akka" thread from a couple
of months ago, and it caught my eye because several people discussed
exactly the sort of thing I'm researching right now: verifying that
actor-based programs conform to some given protocol. In particular, I'm
trying to figure out how we can do better for real-world programs instead
of the simple examples used in things like session types.

I'm currently in the process of collecting more examples of this sort of
problem, so I'd love to know what examples members of this list might have
(particularly examples with publicly accessible code). I'm interested in
any examples of a protocol that can be tricky to implement, and
communication bugs that could have been caught earlier if only there were
some type system/analysis/tool to detect them.

I'm using "protocol" here in a loose sense - it doesn't have to be a
standard, like an RFC. I'm referring more generally to an expectation of
the kinds of messages a process should send or receive - much like the sort
of thing UBF checks for.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20141029/57252dba/attachment.htm>


More information about the erlang-questions mailing list