<div dir="ltr">I would be also interested in this. Please keep me in the loop.</div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Jan 14, 2016 at 9:34 AM, Tristan Tarrant <span dir="ltr"><<a href="mailto:ttarrant@redhat.com" target="_blank">ttarrant@redhat.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello Jakub,<br>
<br>
not only are we interested: we have been talking about it for a while,<br>
but lack of time has not allowed us to pursue it.<br>
So yes, it would be very useful. As far as scope it seems like you<br>
already have a good grasp of what to tackle, and we are more than happy<br>
to answer any questions you might have.<br>
I would like both Bela Ban and Richard Achmatowicz to add their thoughts<br>
to this, as they have more intimate knowledge with the tools and the<br>
concepts behind formal verification.<br>
<br>
Tristan<br>
<div class="HOEnZb"><div class="h5"><br>
On 13/01/2016 16:56, Jakub Senko wrote:<br>
> Hi all!<br>
><br>
> I'm considering a thesis topic [1] inspired by the successful use<br>
> of automated formal verification methods by Amazon engineers for AWS S3 and others [2].<br>
><br>
> The basic idea is to use similar tools to verify core parts of Infinispan<br>
> by constructing a simplified model (because of the state space explosion).<br>
> Most useful areas seem to be the transport layer, command object execution<br>
> (get, put, topology change, state transfer), entry locks etc.<br>
> On the other hand, I'd exclude transactional operations<br>
> which would be too complicated/costly to verify.<br>
><br>
> Do you think this would be useful for you as the infinispan developers?<br>
> Do you have suggestions on what (not) to focus?<br>
> I'd be happy for any comments.<br>
><br>
> Cheers,<br>
> Jakub Senko<br>
><br>
> [1] <a href="https://diplomky.redhat.com/topic/show/355/formal-design-of-distributed-hash-table" rel="noreferrer" target="_blank">https://diplomky.redhat.com/topic/show/355/formal-design-of-distributed-hash-table</a><br>
> [2] <a href="http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/fulltext" rel="noreferrer" target="_blank">http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/fulltext</a><br>
> _______________________________________________<br>
> infinispan-dev mailing list<br>
> <a href="mailto:infinispan-dev@lists.jboss.org">infinispan-dev@lists.jboss.org</a><br>
> <a href="https://lists.jboss.org/mailman/listinfo/infinispan-dev" rel="noreferrer" target="_blank">https://lists.jboss.org/mailman/listinfo/infinispan-dev</a><br>
><br>
<br>
</div></div><span class="HOEnZb"><font color="#888888">--<br>
Tristan Tarrant<br>
Infinispan Lead<br>
JBoss, a division of Red Hat<br>
</font></span><div class="HOEnZb"><div class="h5">_______________________________________________<br>
infinispan-dev mailing list<br>
<a href="mailto:infinispan-dev@lists.jboss.org">infinispan-dev@lists.jboss.org</a><br>
<a href="https://lists.jboss.org/mailman/listinfo/infinispan-dev" rel="noreferrer" target="_blank">https://lists.jboss.org/mailman/listinfo/infinispan-dev</a><br>
</div></div></blockquote></div><br></div>