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
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

11:00 - 12:30: Morning talks 2ARRAY at Vertex WS218
Chair(s): Martin ElsmanDepartment of Computer Science, University of Copenhagen
11:00 - 11:30
An ELI-to-C Compiler: Design, Implementation and Performance
Hanfeng ChenMcGill University, Wai-Mee Ching, Laurie HendrenMcGill University, Canada
DOI File Attached
11:30 - 12:00
Array Programming in Whiley
David J. PearceVictoria University of Wellington
DOI File Attached
12:00 - 12:30
Flexible Data Views: Design and Implementation
Leo OsvaldPurdue University, USA, Tiark RompfPurdue University
DOI File Attached