I would be also interested in this. Please keep me in the loop. On Thu, Jan 14, 2016 at 9:34 AM, Tristan Tarrant <ttarr...@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@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@lists.jboss.org > https://lists.jboss.org/mailman/listinfo/infinispan-dev >
_______________________________________________ infinispan-dev mailing list infinispan-dev@lists.jboss.org https://lists.jboss.org/mailman/listinfo/infinispan-dev