[infinispan-dev] Formal verification (thesis)

[Sebastian Laskawiec]

I would be also interested in this. Please keep me in the loop.

On Thu, Jan 14, 2016 at 9:34 AM, Tristan Tarrant <ttarrant at redhat.com>
wrote:

> 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
> _______________________________________________
> infinispan-dev mailing list
> infinispan-dev at lists.jboss.org
> https://lists.jboss.org/mailman/listinfo/infinispan-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.jboss.org/pipermail/infinispan-dev/attachments/20160114/aaf976e4/attachment-0001.html