TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 16131

Language Based Verification Tools for Functional Programs

( Mar 28 – Apr 01, 2016 )

(Click in the middle of the image to enlarge)

Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/16131

Organizers

Contact



Schedule

Motivation

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.


Summary

Tis report summarizes the program and the outcomes of Dagstuhl Seminar 16131 "Language Based Verification Tools for Functional Programs", organized by:

  • Marco Gaboardi, School of Computing, University of Dundee, UK
  • Suresh Jagannathan, Purdue University, USA
  • Ranjit Jhala, University of California, San Diego, USA
  • Stephanie Weirich, University of Pennsylvania, USA.

The web, multi-core and "big-data" revolutions have been largely built on higher-order programming constructs pioneered in the Functional Programming community. Despite the increasing importance of such programs, there are relatively few tools that are focussed on ensuring that functional programs possess crucial correctness properties. While language based verification for imperative and first-order programs has been studied for decades yielding important ideas like Floyd-Hoare Logics, Abstract Interpretation, and Model Checking. It is only relatively recently, that researchers have proposed language based verification tools {e.g. advanced type systems, contract systems, model checking and higher-order program analyses for functional and higher-order programs.

We organised this seminar to bring together the different schools of researchers interested in software reliability, namely, the designers and implementers of functional programming languages, and experts in software verification, in order create a larger community of researchers focused on this important goal, to let us compare the strengths and limitations of different approaches, to find ways to unite both intellectually, and via tools the complementary advantages of different techniques, and to devise challenging open problems and application areas where verification may be most effective.To this end, the seminar comprised a program of 30 talks from the leading experts on the above topics, and breakout sessions on:

  1. Integrating formal methods tools in the curriculum
  2. Hands on Tool Tutorials
  3. User Interaction
  4. Types and Effects
Copyright Marco Gaboardi, Suresh Jagannathan, Ranjit Jhala, and Stephanie Weirich

Participants
  • Andreas Martin Abel (Chalmers UT - Göteborg, SE) [dblp]
  • Amal Ahmed (Northeastern University - Boston, US) [dblp]
  • Andrew W. Appel (Princeton University, US) [dblp]
  • Lennart Augustsson (Standard Chartered Bank - London, GB) [dblp]
  • Edwin Brady (University of St. Andrews, GB) [dblp]
  • Iavor Diatchki (Galois - Portland, US) [dblp]
  • Richard A. Eisenberg (University of Pennsylvania - Philadelphia, US) [dblp]
  • Jean-Christophe Filliâtre (CNRS & University Paris Sud, FR) [dblp]
  • Cormac Flanagan (University of California - Santa Cruz, US) [dblp]
  • Marco Gaboardi (SUNY - Buffalo, US) [dblp]
  • Deepak Garg (MPI-SWS - Saarbrücken, DE) [dblp]
  • Michael Greenberg (Pomona College - Claremont, US) [dblp]
  • Reiner Hähnle (TU Darmstadt, DE) [dblp]
  • Catalin Hritcu (INRIA - Paris, FR) [dblp]
  • Suresh Jagannathan (Purdue University - West Lafayette, US) [dblp]
  • Ranjit Jhala (University of California - San Diego, US) [dblp]
  • Gowtham Kaki (Purdue University - West Lafayette, US) [dblp]
  • Gabriele Keller (UNSW - Sydney, AU) [dblp]
  • Naoki Kobayashi (University of Tokyo, JP) [dblp]
  • Ekaterina Komendantskaya (University of Dundee, GB) [dblp]
  • Martin Lange (Universität Kassel, DE) [dblp]
  • K. Rustan M. Leino (Microsoft Corporation - Redmond, US) [dblp]
  • Conor McBride (University of Strathclyde - Glasgow, GB) [dblp]
  • Jan Midtgaard (Technical University of Denmark - Lyngby, DK) [dblp]
  • Chih-Hao Luke Ong (University of Oxford, GB) [dblp]
  • Dominic Orchard (University of Cambridge, GB) [dblp]
  • Brigitte Pientka (McGill University - Montreal, CA) [dblp]
  • Ruzica Piskac (Yale University, US) [dblp]
  • Nadia Polikarpova (MIT - Cambridge, US) [dblp]
  • Scott Smith (Johns Hopkins University - Baltimore, US) [dblp]
  • Matthieu Sozeau (University Paris-Diderot, FR) [dblp]
  • Wouter Swierstra (Utrecht University, NL) [dblp]
  • Tachio Terauchi (JAIST - Ishikawa, JP) [dblp]
  • Sam Tobin-Hochstadt (Indiana University - Bloomington, US) [dblp]
  • Hiroshi Unno (University of Tsukuba, JP) [dblp]
  • David Van Horn (University of Maryland - College Park, US) [dblp]
  • Niki Vazou (University of California - San Diego, US) [dblp]
  • Stephanie Weirich (University of Pennsylvania - Philadelphia, US) [dblp]
  • Nobuko Yoshida (Imperial College London, GB) [dblp]

Classification
  • programming languages / compiler
  • verification / logic

Keywords
  • Verification
  • Dependent Types
  • Refinement Types
  • SMT Solvers
  • Higher-Order Program Analysis