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.

Dr Mark Utting

Mark is a senior lecturer in ICT at the University of the Sunshine Coast. His research interests are in formal methods, including formal verification and model-based testing. He is a co-author for the widely acclaimed book “Practical Model-Based Testing: A Tools Approach“. You can find more about Mark on his homepage.

Wei Hua (2019). Wei completed his final year project working on a compiler backend for Web Assembly (Wasm). This is a binary instruction format designed for efficient execution within the browser that is supported in Google Chrome, Mozilla Firefox, Apple Safari, and Microsoft Edge. The underlying machine is comparable, in some ways, to the Java Virtual Machine. For example, it is a stack-based VM which provides built-in support for stack frames and local variables. However, WebAssembly currently provides no support for managing heap memory and relies on user-implemented allocators. Wei faced many challenges compiling Whiley programs to WebAssembly, including the representation of composite data structures (e.g. arrays and records) and the implementation of value semantics and lambdas. Wei managed to successfully implement almost the entirety of the Whiley language, and demonstrated this by passing almost 100% of the test suite supplied with the Whiley Compiler. In addition, he showed a number of the Whiley benchmarks running successfully in WebAssembly and, during his final presentation, demonstrated Conway’s Game of Life running in the browser. Read more here.

Dylan Kumar (2019). Dylan completed his final year project working on a compiler backend for the Ethereum Virtual Machine (EVM). Ethereum provides a turing-complete virtual machine for executing smart contracts which is both extremely low-level and notoriously vulnerable to attack. Since the EVM provides very little support (e.g. compared with the JVM), Dylan faced many challenges compiling Whiley programs for it. These included the layout of both stack memory (for stack frames) and heap memory (for composite data structures such as arrays and records). Dylan demonstrated his implementation using the existing test suite shipped with the Whiley Compiler. Read more here.

Min Hsien (Sam) Weng (2019). Sam completed his PhD in 2019 entitled “Efficient Compilation of a Verification-friendly Programming Language”. His goal was to develop techniques to efficiently compile Whiley for low-level architectures using C as an intermediate target. His thesis focuses on building a compiler for Whiley to produce efficient C code to run fast and for long periods on general operating systems as well as limited-resource embedded devices. It uses static copy elimination analysis to reduce unnecessary array copies, and creates a new algorithm to solve the memory aliasing de-allocation problem using a mixture of static and dynamic analysis techniques. This has less overhead than the traditional reference counting technique used in garbage collection. Read more here.

Janice Chin (2018). Janice completed her final year project working on an implementation of the widely-used QuickCheck tool for Whiley. This is an automated testing tool which generates input values for a function or method based on its type signature and precondition, and then checks the outputs against its postcondition. Janice implemented a number of optimisations to improve the overall performance, including the use of integer range analysis to reduce the number of inputs values generated. She also demonstrated her tool was capable of finding bugs in existing Whiley programs, including in the Whiley Standard Library!! Read more here.

Simon Pope (2018). Simon completed his final year project working a tool for inferring loop invariants from function postconditions. Specifically, it applies the weakest precondition transformer to back propagate a postcondition until a loop is encountered. Then, it applies a range of mutations in an effort to find a loop invariant for which verification succeeds. The basis for this work was an existing paper by Furia & Meyer, though Simon implemented a number of improvements. Read more

Baptiste Pauget (2017). Baptiste worked on prototyping an FPGA backend for Whiley. Specifically, this compiles Whiley programs to VHDL which can then be synthesised for an FPGA. Our Papilio board was used for testing, and small Whiley functions were executed on it. A key feature of Baptiste’s approach was the use of explicit stage statements for breaking up a sequential function into a pipeline. Baptiste’s project demonstrated the potential for running Whiley on an FPGA. Read more
here and here.

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 …