Write a Blog >>
Sun 18 Jun 2017 11:30 - 12:00 at Vertex WS218 - Morning talks 2 Chair(s): Martin Elsman

Arrays are a fundamental mechanism for developing and reasoning about programs. Using them, one can easily encode a range of important algorithms from various domains, such as for sorting, graph traversal, heap manipulation and more. However, the encoding of such problems in traditional languages is relatively opaque. That is, such programming languages do not allow those properties important for the given problem to be encoded within the language itself and, instead, rely up on programmer-supplied comments.

This paper explores how array-based programming is enhanced by programming languages which support specifications and invariants over arrays. Examples of such systems include Dafny, Why3, Whiley, Spec# and more. For this paper, we choose Whiley as this language provides good support for array-based programming. Whiley is a programming language designed for verification and employs a verifying compiler to ensure that programs meet their specifications. A number of features make Whiley particularly suitable for array-based programming, such as type invariants and abstract properties. We explore this through a series of worked examples.

Slides (slides.pdf)97KiB

David (@whileydave) graduated with a PhD from Imperial College London in 2005, and took up a lecturer position at Victoria University of Wellington, NZ. David’s PhD thesis was on efficient algorithms for pointer analysis of C, and his techniques have since been incorporated into GCC. His interests are in programming languages, compilers and static analysis.

Since 2009, he has been developing the Whiley Programming Language (whiley.org) which is designed specifically to simplify program verification. Prior to that, David developed the Java Compiler Kit (JKit), which is an open source Java Compiler aimed at simplifying static analysis.

David has previously interned at Bell Labs, New Jersey, where he worked on compilers for FPGAs; and also at IBM Hursely, UK, where he worked with the AspectJ development team on profiling systems.

Sun 18 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

11:00 - 12:30
Morning talks 2ARRAY at Vertex WS218
Chair(s): Martin Elsman Department of Computer Science, University of Copenhagen
11:00
30m
Talk
An ELI-to-C Compiler: Design, Implementation and Performance
ARRAY
Hanfeng Chen McGill University, Wai-Mee Ching , Laurie Hendren McGill University, Canada
DOI File Attached
11:30
30m
Talk
Array Programming in Whiley
ARRAY
David J. Pearce Victoria University of Wellington
DOI File Attached
12:00
30m
Talk
Flexible Data Views: Design and Implementation
ARRAY
Leo Osvald Purdue University, USA, Tiark Rompf Purdue University
DOI File Attached