28.03.16 - 01.04.16, Seminar 16131
Language Based Verification Tools for Functional Programs
The following text appeared on our web pages prior to the seminar, and was included as part of the invitation.
This Dagstuhl Seminar is motivated by two converging trends in computing. First, the increasing reliance on software has led to an increased interest in seeking formal, reliable means of ensuring that programs possess crucial correctness properties. Second, the rise of the web, multicore, and “big data” has led to a dramatic increase in higher-order functional languages that are seeing a dramatic uptick in adoption, either directly (e.g. Scala, Haskell, F#, Clojure), or via the incorporation of functional features - first-class functions, parametric polymorphism, immutability, algebraic datatypes and so on - in imperative languages, both legacy (e.g. Java, C++) and emerging (e.g. Python, Swift, Rust).
In theory, functional programs are ideal for language based verification. They offer a rich semantic structure that allows the description of different correctness properties in a natural way. They provide a powerful abstraction mechanism – first class functions – that is helpful to construct programs and verify correctness properties in a modular way. They emphasize programming without pervasive mutation and side-effects which promotes mathematical (e.g. algebraic) reasoning. In practice, however, while the research community has studied the problem of language based verification for imperative and first-order programs for decades – yielding important ideas like Floyd-Hoare Logics, Abstract Interpretation, Model Checking, and Separation Logic and so on – it is only relatively recently, that proposals have emerged for language based verification tools for functional and higher-order programs.
These techniques include advanced type systems, contract systems, model checking and program analyses specially tailored to exploit the structure of functional languages. These proposals are from groups based in diverse research communities, attacking the problem from different angles, yielding techniques with complementary strengths. All the above methods let the programmer specify fine-grained properties that the program should satisfy, and then verify that in a given implementation, data and program components are used in a way that meets the specification. However, they differ widely in trade-offs made between the expressiveness of the specifications and automation of the verification. At one end of the spectrum, dependent type systems are extremely expressive, but require the programmer to provide proofs, while at the other end program analyses are limited to finite state specifications but are fully automatic.
The overall goal of this seminar is to bring together researchers working in all related areas so that we may
- compare the strengths and limitations of the different approaches,
- discuss ways to unify the complementary advantages of different techniques, both conceptually and in tools,
- share challenging open problems and application areas where verification may be most effective,
- identify novel ways of using verification techniques for other software engineering tasks such as code search or synthesis, and
- improve the pedagogy and hence adoption of such techniques.
In other words, the aim of this Dagstuhl Seminar is to catalyze the creation of a larger community of researchers working on the above topics, thereby accelerating the research and adoption of language based verification for functional programs.