In the past decade, significant progress has been made towards design and development of efficient concurrent data structures and algorithms, which take full advantage of parallel computations. Due to sophisticated interference scenarios and a large number of possible interactions between concurrent threads, working over the same shared data structures, ensuring full functional correctness of concurrent programs is challenging and error-prone.
In my talk, through a series of examples, I will introduce Fine-grained Concurrent Separation Logic (FCSL)---a mechanized logical framework for implementing and verifying fine-grained concurrent programs.
FCSL features a principled model of concurrent resources, which, in combination with a small number of program and proof-level commands, is sufficient to give useful specifications and verify a large class of state-of-the-art concurrent algorithms and data structures. By employing expressive type theory as a way to ascribe specifications to concurrent programs, FCSL achieves scalability: even though the proofs for libraries might be large, they are done just once.
Deepak D'Souza (Indian Institute of Science)
A high-level race occurs when an execution interleaves instructions corresponding to user-annotated critical accesses to shared memory structures. Such races are good indicators of atomicity violations. We propose a technique for detecting *all* high-level dataraces in a system library like the kernel API of a real-time operating system (RTOS) that relies on flag-based scheduling and synchronization. Our methodology is based on model-checking, but relies on a meta-argument to bound the number of task processes needed to orchestrate a race. We describe our approach in the context of FreeRTOS, a popular RTOS in the embedded domain.
This is joint work with Suvam Mukherjee and S. Arun Kumar.
Prof Stephen Muggleton FREng (Imperial College London)
Computer Science is the symbolic science of programming, incorporating techniques for representing and reasoning about the semantics, correctness and synthesis of computer programs. Recent techniques involving the learning of deep neural networks has challenged the "human programmer" model of Computer Science by showing that bottom-up approaches to program synthesis from sensory data can achieve impressive results ranging from visual scene analysis, expert level play in Atari games and world-class play in complex board games such as Go. Alongside the successes of Deep Learning increasing concerns are being voiced in the public domain concerning the deployment of fully automated systems with unexpected and undesirable behaviours. In this presentation we will discuss the state-of-the-art and future challenges of Machine Learning technologies which promise the transparency of symbolic Computer Science with the power and reach of sub-symbolic Deep Learning. We will discuss both weak and strong integration models for symbolic and sub-symbolic Machine Learning.
Bio: Stephen H. Muggleton FBCS, FIET, FAAAI, FECCAI, FSB, FREng is Professor of Machine Learning and Head of the Computational Bioinformatics Laboratory at Imperial College London. Stephen Muggleton is currently Director of the Syngenta University Innovation Centre at Imperial College and holds a Royal Academy of Engineering/Syngenta Research Chair. He received his Bachelor of Science degree in Computer Science (1982) and Doctor of Philosophy in Artificial Intelligence (1986) supervised by Donald Michie at the University of Edinburgh. Following his PhD, Prof. Muggleton went on to work as a postdoctoral research associate at the Turing Institute in Glasgow (1987–1991) and later an EPSRC Advanced Research Fellow at Oxford University Computing Laboratory (OUCL) (1992–1997) where he founded the Machine Learning Group. In 1997 he moved to the University of York and in 2001 to Imperial College London.
Andrey Mokhov (Newcastle)
Most build systems start small and simple, but over time grow into hairy monsters that few dare to touch. As we demonstrate in this talk, there are a few issues that cause build systems major scalability challenges, and many pervasively used build systems (e.g. Make) do not scale well.
We use functional programming to design abstractions for build systems, and implement them on top of the Shake library, which allows us to describe build rules and dependencies. To substantiate our claims, we engineer a new build system for the Glasgow Haskell Compiler. The result is more scalable, faster, and spectacularly more maintainable than its Make-based predecessor
23rd November: Computer Science as an Application Domain for Data Science
Colin Johnson (Kent)
The last few years have witnessed a revolution in the application of data science across many aspects of human endeavour. However, the application back to problems in computer science itself has been rather thin. This talk will explore this issue in general, and discuss some examples of and opportunities for the application of data science to computer science and software development. This will include a number of examples, e.g. of the application of information-theoretic learning to fault localisation.
Bio: Colin Johnson is Associate Dean of Sciences and Reader in Computer Science at the University of Kent. His research interests are in the areas of machine learning and data mining, both in the development of new methods in those areas and in their applications, in areas such as bioinformatics, engineering, and digitial humanities. Recently, he has been investigating how data science techniques can be used in areas such as mathematics and software development.
Dick Whittington (RAEng visiting professor, York)
Throughout their technical education, engineers of all flavours build up a knowledge of technologies and the techniques and processes that make them work. But starting a business – or contributing effectively to an early stage business – or injecting innovation into an existing business – needs more than that. To contribute effectively to a business, it’s necessary also to know about notions of product, platform and service, about customers and ecosystems, about markets and their dynamics, about intellectual property and its protection, about risk, company finance, investment, governance and legal requirements; and above all, about what’s needed to create and scale something of value. This seminar explains how the Business Innovation course is addressing that gap, for students and staff anticipating an adventure into business. It will do this with reference to both the national and local economic context, and future options for the course.
Bio: Dick is a serial entrepreneur, business mentor and investor, with over 30 years of experience in business. He is co-founder of MooD International, a software business recognised through multiple Queen’s Awards: two for Innovation, and a third for International Trade. The company was voted “York Business of the Year” for 2015. In 2012 Dick was elected Fellow of the Royal Academy of Engineering. He plays an active role within the Academy, including within its successful Enterprise Hub where he acts as mentor for new spin-out technology companies. Funded by the Academy, in 2015 Dick was appointed Visiting Professor of Business Innovation at the University of York. He is also an active mentor and angel investor within several London and regional technology accelerator programmes.
Andrea Manca (Centre for Health Economics, York)
Person-centred healthcare (sometimes referred to as personalised medicine, precision medicine, etc.) is becoming one of the hottest topics on the public/private agenda worldwide. It has supporters among the industry, patients organisations, healthcare professionals, academics, funders and politicians. Thus, devoting energies and resources to pursue (and hopefully realise) the promises of person-centred healthcare would seem to be a win-win strategy for a number of stakeholders. Indeed, recent years have seen an acceleration in R&D efforts towards the development of novel person-centred diagnostics, drugs and medical devices (both therapeutic and support). But here lies the critical issue: how can Society shape the future of healthcare, identify and prioritise R&D investments towards acceptable, cost-effective and sustainable person-centred interventions with the highest return in terms of population health and other relevant outcomes? Cost-Effectiveness Analysis (CEA) for Health Technology Assessment (HTA) plays a pivotal role in informing such decisions in many jurisdictions around the world. This talk begins by describing the standard CEA framework and its use in HTA to inform R&D and technology adoption decisions in the UK and elsewhere. It then discusses the challenges of applying standard CEA methods to the evaluation of person-centred healthcare technologies, and provides examples of how these issues can be addressed. This talk may be of interest to researchers in Biology, Chemistry, Electronics, Computer Sciences and Physics who are actively pursuing initiatives into the area of new healthcare technologies or are potentially considering doing so. It is intended to be an opportunity for the audience to find out how health economics can support the translation of (clinically and patient-centred) relevant aspects of their research into the healthcare technologies of the future, hopefully opening up new collaborations and furthering the University of York vision towards interdisciplinarity of its research focus.
Michael Cook (University of Falmouth)
For most people working in AI and games these days the key word is 'superhuman'. How can we build AI to beat humans at Go, at Poker, at Starcraft? In Computational Creativity - a subfield of AI where people design software to paint, write poetry and design videogames - there's a more pressing question: why would anyone care what an AI did, anyway? In this talk I'll discuss the brief history of Computational Creativity; the software soupmaker that has no friends; the AI game designer that never tidies up; and the missing piece in today's AI narrative: failure.
Simon Dobson (St Andrews)
Sensor systems are increasingly important in providing robust, reliable, rich information to support scientific and policy activities. Obtaining that robustness, reliability, and richness, however, requires that we develop mechanisms for analysing the sensed data as it arrives, and for fitting it into a wider interpretive context that can be used by scientists and decision-makers. In this talk we discuss these challenges and explore a couple of approaches we've been investigating to improve our understanding of sensor systems as they degrade, and to improve the ways in which we classify sensor observations against expectations.
Bio: Simon Dobson is Professor of Computer Science at the University of St Andrews. He works on complex and sensor systems, especially on sensor analytics and the modelling of complex processes. His work has given rise to over 150 peer-reviewed papers and to leadership roles in research grants worth over £30M, most recently as part of a £5M EPSRC-funded programme grant in the Science of Sensor Systems Software. He was also the founder and CEO of a research-led start-up company. He holds a BSc and DPhil in computer science, is a Chartered Fellow of the British Computer Society, a Chartered Engineer and Senior Member of the IEEE and ACM.
Leandro Indrusiak (York)
Wormhole switching is a widely used network protocol, mostly because the small buffering requirements it imposes on each network router, which in turn results in low area and energy overheads. For instance, this is of key importance in multi-core and many-core processors based on networks-on-chip (NoC), as the area and energy share of the on-chip network itself can reach up to 30% of the area and energy used by the whole processor. However, the nature of wormhole switching allows a single packet to simultaneously acquire multiple links as it traverses the network, which can make worst-case packet latencies hard to predict. This becomes particularly severe in large and highly congested networks, where complex interference patterns become the norm. Still, worst case latency prediction models are needed if one needs to make such systems amenable to real-time applications.
Different link arbitration mechanisms can result in different worst-case latency prediction models, and recent research has addressed NoCs with TDM, round-robin and priority arbitration. In this talk, I will focus on priority-preemptive wormhole NoCs. I will give a detailed account of the architectural features that can support that type of arbitration in NoCs, and will review the latest research on analytical methods aimed at predicting worst-case packet latency over such networks. I will then show opportunities and advantages of using priority-preemptive NoCs in the domains of multi-mode, mixed-criticality and secure systems, where the trade-off between flexibility and predictability that is inherent to such networks can be fully exploited.
Bio: Leandro Soares Indrusiak is a faculty member of University of York's Computer Science department since 2008, and currently holds a readership. He is a member of the Real-Time Systems (RTS) research group, and his current research interests include on-chip multiprocessor systems, distributed embedded systems, resource allocation, cloud computing, and real-time networks, having published more than 120 peer-reviewed papers in the main international conferences and journals covering those topics (seven of them received best paper awards). He has graduated seven doctoral students over the past ten years, and currently supervises three doctoral students and three post-doc research associates.
He graduated in Electrical Engineering from the Federal University of Santa Maria (UFSM) in 1995 and obtained a MSc in Computer Science from the Federal University of Rio Grande do Sul (UFRGS), Porto Alegre, in 1998. He held a tenured assistant professorship at the Informatics department of the Catholic University of Rio Grande do Sul (PUCRS) in Uruguaiana from 1998 to 2000. His PhD research started in 2000 at UFRGS and extended his MSc work on design automation environments for microelectronic circuits. From 2001 to 2008 he worked as a researcher at the Technische Universität Darmstadt, Darmstadt, Germany, where he finished his PhD and then lead a research group on System-on-Chip design. His binational doctoral degree was jointly awarded by UFRGS and TU Darmstadt in 2003.
He is the principal investigator of EU-funded SAFIRE and DreamCloud projects, and a co-investigator in a number of other funded projects. He has held visiting faculty positions in five different countries, is a member of the HiPEAC European Network of Excellence, and a senior member of the IEEE.
Ioannis Darzentas (Leverhulme Visiting Professor)
Are the problems Design deals with always complex? or sometimes are they simply complicated. This talk will briefly introduce Systems Thinking as a way of tackling complex design problem spaces. The thesis is that at least the human centric ones (which by far are the majority) are always complex. Design Thinking in most cases acknowledges complexity but it has a paucity of methods to deal with it. Service Design will be introduced as a rapidly emerging area of human centric design. Service Design is naturally complex and a prime paradigm that gains from adopting Systems Thinking for Design problem space capturing, understanding and for moving towards praxis. An important outcome of our research, has been to reorient the focus of the Design Intervention in that products (tangible or intangible) are byproducts of Service Design.
Researchers in human-computer interaction (HCI) have long been interested in the problem of system security, particularly from the point of view of the usability of authentication systems. Angela Sasse coined the well known adage that “users are not the enemy” in the development of secure systems. However it is interesting that research in HCI has largely focussed on very specific parts of the authentication process, for example analysing the kinds of passwords people create, the kinds of potentially insecure behaviours they undertake in relation to passwords and so on. I can find no researchers who have thought about the password creation system (PCS) as a small interactive system (which is what HCI researchers study all the time) which can be studied for its usability and user experience. An obvious implication if one thinks of PCSs in this way is that if the system has poor usability, more cognitive effort will be required by users to understand how the system works, which will lead to less cognitive effort being available to create good passwords. In this talk I will outline our understanding of the PCS as an interactive system and discuss some of the work I had undertaken with two PhD students to unpack the implications of approaching the topic in this way.