2016 competition
Winner
Verification of Message-Passing Concurrent Systems
Emanuele D'Osualdo, University of Oxford
As our world keeps delegating more and more critical tasks to networks of interconnected machines, developing a strong theoretical framework for their design and analysis is of paramount importance.
This dissertation is concerned with the development of fully-automatic methods of verification, for message-passing-based concurrent systems.
First, we define a sound parametric analysis for Erlang, an industrial-strength programming language. Thanks to a combination of abstraction and infinite-state model-checking, our prototype implementation, called Soter, is able to prove properties of Erlang programs such as unreachability of error states, mutual exclusion or bounds on mailboxes.
The resulting analysis however has a blind spot: it is not able to precisely represent reconfigurable systems, i.e. systems where the communication network changes over time. To fix this, the second part of the thesis develops a novel type system for the analysis of the communication topology of pi-calculus processes.
View Emanuele D'Osualdo's dissertation | Watch the video
Highly commended
Pushing the Limits of Indoor Localisation in Today’s Wi-Fi Networks
Jie Xiong, University College London
Wireless networks are ubiquitous nowadays and play an increasingly important role in our everyday lives. A lot of emerging applications including indoor navigation, augmented reality, gesture recognition and human tracking heavily rely on and require an even more sophisticated Wi-Fi network.
One key component for the success of these applications is accurate localization. While we have GPS in the outdoor environment, indoor localization at a sub-meter granularity remains challenging due to a number of factors, including the presence of strong wireless reflections indoors and the burden of deploying and maintaining any additional location service infrastructure.
The recent trend of dramatically increasing the number of antennas and of higher bandwidths at the Wi-Fi access points brings us unique opportunities to significantly improve the accuracy of indoor localization. Two indoor localization systems are introduced in this dissertation.
ArrayTrack is the first localization system hosted on Wi-Fi infrastructure which is able to achieve an accuracy below 30 cm via a novel reflection-path identification scheme. ToneTrack is another system, which breaks the bandwidth limit on time-based localization by combining data from adjacent channels.
Highly commended
Visualizing Set Relations and Cardinalities Using Venn and Euler Diagrams
Luana Micallef, University of Kent
In medicine, genetics, criminology and various other areas Venn and Euler diagrams are used to visualize data-set relations and their cardinalities. The data sets are represented by closed curves and the data-set relationships are depicted by the overlaps between these curves. Both the sets and their intersections are easily visible, as the closed curves are pre-attentively processed and form common regions that have a strong perceptual grouping effect. Besides set relations such as intersection, containment and disjointness, the cardinality of the sets and their intersections can also be depicted in the same diagram (referred to as area-proportional) through the size of the curves and their overlaps. Size is a pre-attentive feature and so similarities, differences and trends are easily identified. Thus such diagrams facilitate data analysis and reasoning about the sets. However, drawing these diagrams manually is difficult, often impossible, and current automatic drawing methods do not always produce appropriate diagrams.
This dissertation presents novel automatic drawing methods for different types of Euler diagrams and a user study of how such diagrams can help probabilistic judgement. The main drawing algorithms are eulerForce, which uses a force-directed approach to lay out Euler diagrams, and eulerAPE, which draws area-proportional Venn diagrams with ellipses. The user study evaluated the effectiveness of area-proportional Euler diagrams, glyph representations, Euler diagrams with glyphs and text-plus-visualization formats for Bayesian reasoning, and a method eulerGlyph was devised to automatically and accurately draw the assessed visualizations for any Bayesian problem. Additionally, analytic algorithms that instantaneously compute the overlapping areas of three general intersecting ellipses are provided, together with an evaluation of the effectiveness of ellipses in drawing accurate area-proportional Venn diagrams for three-set data and of the characteristics of the data that can be depicted accurately with ellipses.
