Verifying Java 8 Streams

title:Verifying Java 8 Streams
keywords:verification, logics, Java 8, functional
topics:Languages, Logics and semantics
contact:prof.dr. M. Huisman & W.H.M. Oortwijn MSc


Description

At the University of Twente we are building and maintaining the VerCors verification toolset (see [2] for details and for verification examples). VerCors allows to verify different concurrency models of various widely-used languages, including Java and C. However, VerCors lacks support for most of the new language features of Java 8, in particular lambda expressions, functional interfaces, and (as a consequence) streams.

During this research project you will investigate how VerCors can be extended to support anonymous functions (lambda's) and write a proposal for this. To do so you will need to study existing work on annotation languages for lambda's, for example work on higher-order separation logic. A good starting point might be [1]. 

References

  1. Permission-based Separation Logic for Scala (Digital version available here)
  2. VerCors website (Digital version available here)