FLoC (Federated Logic Conference) is a quadrennial two-week event that brings together eight top conferencesapplying methods of logic in computer science, and about 60 workshops. The area is of great importance to computing research: logic provides computer science with both a unifying foundational framework and a tool for modelling computing systems; it has been called ``the calculus of computer science,'' and played a crucial role in diverse areas such as artificial intelligence, computational complexity, distributed computing, database systems, hardware design, programming languages, and software engineering. The research of just over 20% of Turing award winners has been on the application of logic to computer science; in the UK, five of the current eight UKCRC grand challenges are in FLoC areas.The proposal is to enable us to invite top-level researchers to deliver plenaries and tutorials at FLoC, to makeFLoC particularly attractive to students and to make it easier for researchers from the UK and elsewhereto attend FLoC.

Counter automata are a universal computational model that has been studied since the inception of computer science. In particular, counter automata have been intensively studied in automated verification since they can naturally model diverse computational features such as linked data structures, recursion, and unbounded parallelism. This flexibility and expressiveness however makes their algorithmic analysis very challenging. The goal of this project is to develop new automated procedures for analysing counter automata that will ultimately aid the design, modelling, verification, and analysis of complex computer systems. The general area of the project is model checking, which is an approach to the problem of designing complex hardware and software systems. In essence, model checking involves the construction and systematic analysis of abstract mathematical models of systems, ideally at design time, using automated tools. The importance of the area is growing in response to the challenge posed by new technologies such as the cloud, concurrent embedded systems, multi-core hardware, the Internet of Things, Big Data, etc. In many application areas the efficient design and correct functioning of computer systems is both economically critical and safety critical. The significance and scientific challenge of model checking were recognized by bestowal of the 2007 Turing Award to Clarke, Emerson, and Sifakis for their foundational work in the area. This proposal aims to enrich the tool-kit of model checking by developing algorithms and analysis tools for counter automata. One of the major inherent scientific challenges is that model checking involves performing exhaustive analysis of the state spaces of models, whereas counter automata are inherently infinite-state devices that have universal computing power. Another significant challenge is that we will be considering counter automata with additional features, such as parameters and probabilistic behaviour. To meet this challenge we will build on a body of techniques developed over the past two decades, making use of powerful abstractions and rich logical theories of arithmetic which allow us symbolically to represent and reason about infinite state spaces in a finite way. Outcomes of the project will include new algorithms to help analyse counter automata as well as an open-source tool for solving arithmetic constraints that arise in such analysis. There is already a wide variety of highly effective tools for analysing counter automata, including Petri nets. Our goal is that the outcomes of this grant will enhance the capabilities of the next generation of these tools.

Individuals are increasingly reliant on digital applications and services to store photos, documents, notes and other valued personal data. They are also accustomed to - and tacitly accept as a hidden cost of using otherwise 'free' services - these applications amassing activity data and metadata from which companies derive significant business value. For example, Facebook makes much of its £22bn yearly revenue by being able to precisely target advertisements to users by deciphering their unique preferences from their likes, tags, contacts, updates, photos, travel patterns etc (some accessed through permissions to Facebook via other apps) [BBC]. There is a highly lucrative, if shadowy, trafficking in users' data: data brokering companies such as Acxiom and Epsilon compile thorough dossiers on people's physical and mental health conditions, sexual orientation, personal vices, and vulnerabilities to aid companies in identifying likely consumers [CBS,SCH]. Meanwhile, there are no corresponding tools accessible for individuals to learn about themselves through their personal data. Within recent years, there is a growing literacy around data as a medium for generating information and key insights. This is represented in the Quantified Self movement (see, e.g.: http://feltron.com), with individuals self-tracking their patterns of behaviour, physiological responses, productivity, correspondences etc with a view toward enabling personal reflection and gaining greater self-knowledge [LI]. Wearable activity trackers have been appropriated by some for self-diagnostic purposes: e.g. finding correlations between activities and symptoms to make informed changes to improve personal wellbeing [ROO]. There is untapped potential in applying this sensibility toward broader and deeper personal sense-making by drawing connections between the full diversity of one's personal data currently siloed in various services and applications - from the wide array of web services, to mobile applications, wearable and home IoT devices. Personal Information Management (PIM) is a growing ICT sector with an estimated market worth of £16.5bn [NES]. Focusing on four major activities - keeping, finding, organizing and maintaining - PIM offers valuable insights into how to develop and sustain practices for effectively managing one's own data [KLI]. A particular challenge in developing PIM solutions is the individuality of lay data management techniques and strategies, which map onto people's individual strengths and familiar, established practices; in short, individuals thrive when they are able to develop strategies that work for them and for the particular goals they have defined. Given that many services ostensibly offer information management to users (albeit with pre-set UX constraints), an especially interesting frontier for extending PIM research lies in lifting data out from the applications that are currently managing them to support individualised, goal oriented collection and management of personal data - and further, offering techniques for managing between diverse data types (e.g. the minutia of metadata, narrative/textual data, photographic data, activity data, etc). This project will fill several important gaps in understandings of personal sense-making, including: 1) in contrast to commercial ends for extracting, collecting and analysing people's personal data, understanding what kinds of self-knowledge would offer significant value to individuals, and how bridging personal data between applications and services might uniquely afford these personal insights; and 2) understanding how people can derive meaning from mixed data types and across applications, unbounded by the goal orientations of the individual applications or services they use to capture their personal data.

The goal of computer vision is to impart machines with the ability to see, that is, to understand an image similar to a human. This consists of identifying which object categories are present in an image and where (car, person, trees), their actions (running, driving, sitting), and their relative locations (person inside the car, car above the road). The challenge of computer vision lies in obtaining a powerful discriminative representation of an image that allows us to infer the scene encoded within it. Consider, for instance, the representation of an image as captured by a camera, which consists of color values of each of its pixels. Two images that differ greatly in their color values may still depict the same scene (for example, images of the same location at day and night). At the same time, small changes in the color values may result in a completely different scene where objects have moved considerably. This makes raw color values unsuitable for understanding the scene depicted in the image. Traditional computer vision approaches have relied on hand-designed representations of an image that are more amenable to scene interpretation. Given such a representation, there exist several principled formulations for learning to interpret scenes, which take advantage of the powerful mathematical programming framework of convex optimization. Convex optimization offers many computational advantages: it scales elegantly with the size of the problem, it provides global optimality, it offers convergence guarantees and it can be parallelised over multiple machines without affecting the accuracy. Recent years have seen the rise of deep learning, and specifically convolutional neural networks (CNN), which aim to automatically obtain the representation of visual data from a large training set. While an automated approach is highly desirable due to its scalability, it comes with the challenge of solving highly complex non-convex mathematical programs. The aim of our research is to overcome these challenges by finding connections between convex optimization and deep learning. The key observation is that the non-convex programs encountered in deep learning for computer vision have a special structure that is closely related to convexity. Specifically, while the mathematical programs are not convex, they are of a difference-of-convex (DC) form. A DC program can be optimized efficiently by an iterative algorithm, which, at each iteration, solves a convex optimization problem. Our aim is to exploit the structure of DC-CNNs to design the next generation of algorithms for computer vision. Specifically, we will build customized algorithms that will scale up the dimensionality of the CNN by orders of magnitude while keeping the computational cost low. Our algorithms will retain many of the highly desirable benefits of convex programming (convergence, quality guarantees, elegant scaling, distributed computing) while still allow the automatic estimation of image representations. The impact of such principled and efficient algorithms is potentially huge. The new CNN architectures that this enables will allow researchers to address significantly more complex visual tasks. For example, a generative network that can provide a set of diverse future frames of a given video sequence, or a intelligent agent that can crawl the web for images and videos and complete the captions in order to bridge the gap between visual data and searchable content. Our research results will be made publicly available via open source software. The project is also likely to have a large academic impact, consolidating the leadership of the UK in machine learning and computer vision.

Abstracts are not currently available in GtR for all funded research. This is normally because the abstract was not required at the time of proposal submission, but may be because it included sensitive information such as personal details.