Articles

  • No categories

People

On this page you’ll find details of those people currently involved in the Whiley project.  At the moment, the list is quite small … but we’re always looking for more help!!


Dr David J. Pearce (@whileydave)

David is a senior lecturer in computer science at the School of Engineering and Computer Science, Victoria University of Wellington.  David started the Whiley project in late 2009, and has been working on getting a stable release ever since!

Bio: David  graduated from Imperial College London in 2005, having already taken up a lecturer position at Victoria University of Wellington, NZ. David’s thesis (supervised by Prof. Paul Kelly) 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. David is particularly interested in tools and languages that eliminate software errors. David has previously interned at Bell Labs, New Jersey, where he worked under Oskar Mencer on compilers for FPGAs; and also at IBM Hursley, UK, where he worked under Robert Berry on profiling systems with the AspectJ development team.  You can find more about David on his homepage, including his publications and projects.

A/Prof Lindsay Groves

Lindsay is an Associate Professor in computer science at the School of Engineering and Computer Science, Victoria University of Wellington.  His research interests are in formal methods, particularly with respect to the formal verification of software. You can find more about Lindsay on his homepage.


Sebastian Schweizer (2016). Sebastian’s project was about adding reference lifetimes (as found in e.g. Rust) to Whiley.  The primary purpose was enable to safe deallocation of memory when it is no longer required.  Previously, Whiley assumed some form of garbage collection which made running Whiley programs in certain environments (e.g. embedded systems) difficult.  Sebastian’s project was a success, and reference lifetimes were added to Whiley in v0.3.40. Read More…

Cody Slater (2015). Cody completed his final-year project working on a back-end tool for compiling Whiley code to JavaScript for the browser. This presented various challenges. Cody’s tool compiled from the Whiley Intermediate Language (WyIL) which uses unstructured control flow. In contrast, JavaScript does not support unstructured control-flow. Similarly, there is a large mismatch between types in Whiley and those found in JavaScript. Cody successfully demonstrated his project compiling some simple programs (Minesweeper and Conway’s game of life) and running them in the browser. Read More…

Marc Shaw (2015). Marc completed his final-year project working on a tool for identifying redundant test cases. The project arose from the burgeoning size of the Whiley test suite, and the need to find better ways to manage it. As every new test case is added the chance of it being very similar to an existing one increases. Every additional test case affects the productivity as it increases the time to run through the entire suite, and removing duplicate tests would reduce this. Marc developed a tool which traces program execution to generate a test “finger print” based on the function’s called. The tool then compared finger prints of different tests by measuring edit distance. The tool narrows down the number of candidate tests which may be redundant so that they can subsequently be inspected manually. Read More…

Matt Stevens (2014). Matt completed his final-year project working on a back-end tool for compiling Whiley code to run on the CrazyFlie Quadcopter. This presented a number of unique challenges, such as the limited amount of onboard RAM (20KB). Indeed, many features of Whiley are not well-suited to this task and force the unnecessary use of dynamically allocated memory (such as unbound arithmetic and arbitrary sized lists). To that end, Matt made various compromises to the semantics of Whiley to make the project possible. Despite this, Matt managed to successfully replace one of the CrazyFlie modules with equivalent code written in Whiley. This project also provided useful feedback on the design of Whiley and future directions it should take. Read More…

Henry Wylde (2014). Henry completed his final-year project investigating the use of off-the-shelf SMT solvers for verifying Whiley programs. The project designed and implemented an extension which supported the use of an arbitrary SMT solver with the Whiley compiler (specifically, via SMT-LIB). The project was evaluated using the existing benchmark suites available for Whiley and using the well-known Z3 solver. A large number of simple benchmarks were successfully verified in this manner, though additional work is necessary to tackle the larger examples. Read More…

Melby Ruarus (2013).  Melby completed his final-year project investigating a back-end tool for compiling Whiley programs to OpenCL.  This allows simple Whiley programs to be run on a GPU without modification.  Programs written in Whiley are typically not well suited to execution on GPUs which exhibit large scale data parallelism, compared with a traditional CPU. Therefore, the developed solution attempted to parallelise only the portions of programs which were likely to benefit—specifically, such as certain types of loop. The evaluation of the technique validated the approach with one benchmark exhibiting a 5.2x speed improvement.  Read More…

Arthur Protin (2012). Art worked as a post-doc for six months developing a Whiley-to-C backend, which was subsequently included in the Whiley Development Kit. The goal was to provide an implementation which would translate Whiley programs in a straight-forward fashion into C. As such, no effort was made to ensure the generated C code was efficient. In particular, following Whiley’s use of unbound arithmetic, the generated C code made use of the GNU Multiple Precision library. The project succeeded in getting the majority of Whiley tests to pass.

Timothy Jones (2011).  Tim (@zmthy) completed his final-year project investigating efficient implementations of the Actor model on the JVM for Whiley. The actor model is an attempt to simplify concurrency and reduce the inherent problems of deadlock and race-conditions. The project explored the use of Actors as a concurrency model for Whiley, and employed a novel approach to implementing them on the JVM as lightweight threads. Read More …