[infinispan-dev] Formal verification (thesis)

[Tristan Tarrant]

Hello Jakub,

not only are we interested: we have been talking about it for a while, 
but lack of time has not allowed us to pursue it.
So yes, it would be very useful. As far as scope it seems like you 
already have a good grasp of what to tackle, and we are more than happy 
to answer any questions you might have.
I would like both Bela Ban and Richard Achmatowicz to add their thoughts 
to this, as they have more intimate knowledge with the tools and the 
concepts behind formal verification.

Tristan

On 13/01/2016 16:56, Jakub Senko wrote:
> 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
> _______________________________________________
> infinispan-dev mailing list
> infinispan-dev at lists.jboss.org
> https://lists.jboss.org/mailman/listinfo/infinispan-dev
>

-- 
Tristan Tarrant
Infinispan Lead
JBoss, a division of Red Hat