[infinispan-dev] Formal verification (thesis)

[Jakub Senko]

Hi all!

I'm considering a thesis topic [1] inspired by the successful use
of automated formal verification methods by Amazon engineers for AWS S3 and others [2].

The basic idea is to use similar tools to verify core parts of Infinispan
by constructing a simplified model (because of the state space explosion).
Most useful areas seem to be the transport layer, command object execution
(get, put, topology change, state transfer), entry locks etc.
On the other hand, I'd exclude transactional operations
which would be too complicated/costly to verify.

Do you think this would be useful for you as the infinispan developers?
Do you have suggestions on what (not) to focus?
I'd be happy for any comments.

Cheers,
Jakub Senko

[1] https://diplomky.redhat.com/topic/show/355/formal-design-of-distributed-hash-table
[2] http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/fulltext