Idris: Verified Systems Programming with Dependent Types by Edwin Brady

Systems software, such as an operating system or a network stack, underlies everything we do on a computer, whether that computer is a desktop machine, a server, a mobile phone, or any embedded device. It is therefore vital that such software operates correctly in all situations. In recent years, dependent types have emerged as a promising approach to ensuring program correctness using languages and verification tools such as Agda and Coq. However, these tools operate at a high level of abstraction and so it can be difficult to map these verified programs to efficient low level code, working with bit-level operations and interacting directly with system services.

In this talk I will describe Idris, a dependently typed programming language implemented with systems programming in mind. I will show how it may be used to implement programs which interact safely with the operating system, in particular how to give precise APIs for verifiable systems programming with external C libraries.

Bio: Edwin Brady is a SICSA Advanced Research Fellow at the University of St Andrews
(http://www.cs.st-andrews.ac.uk/~eb)

Event details

  • When: 6th February 2012 14:00 - 15:00
  • Where: Phys Theatre C
  • Series: CS Colloquia Series
  • Format: Colloquium

Responsibility Modelling by Prof Ian Sommerville

Many ‘failures’ in software-intensive organisational systems result from human actions or inaction so, to reduce the possibility of such ‘failures’ and so improve system dependability, it is important to adopt a holistic view where system designers consider the environment in which a system will be used as well as the technical characteristics of the system itself.

In this talk, I will introduce the notion of responsibility modelling, which aims to represent the responsibilities of human and automated agents in a complex system, where the system may be created by integrating different systems from different agencies. The motivation for the work is that many ‘system failures’ are actually failures of agents in the system to fulfil their expected responsibilities and so responsibility modelling offers the opportunity to analyse how responsibilities are distributed and to identify responsibility vulnerabilities, before these lead to system failure.

Bio

 Ian Sommerville has been Professor of Computer Science at St Andrews University since 2006. For more details see http://www.software-engin.com.

Event details

  • When: 13th February 2012 14:00 - 15:00
  • Where: Cole 1.33
  • Series: CS Colloquia Series
  • Format: Colloquium

Evolution of Radio Access Networks: Lighting up IQ by Francisco J. Garcia, Agilent Technologies

In this talk we will introduce how new mobile base station architectures are evolving not only to meet demand but also to become “greener” since at current rates of deployment, mobile networks are becoming very large CO2 contributors. These new base station architectures are also becoming enablers for new Radio Access Networks (RANs) where the same infrastructure can support multiple radio technologies simultaneously by backhauling their baseband leading towards distributed antenna systems and distributed base station architectures. Some would argue that this represents a paradigm shift towards “cloud” enabled mobile networks. In the talk we will cover the reasons why things are progressing this way, how this is being enabled through technology innovation, and what Agilent has done to meet some of the test and measurement challenges in this evolved 4G wireless communications space.

Event details

  • When: 27th February 2012 14:00 - 15:00
  • Where: Phys Theatre C
  • Series: CS Colloquia Series
  • Format: Colloquium

A Decade of Research on Constraint Modelling and Reformulation:The Quest for Abstraction and Automation by Alan M Frisch

Abstract:

To mark the Tenth International Workshop on Constraint Modelling and Reformulation, this talk reviews research in the field over the past decade, focusing on the key themes of abstraction and automation.

Looking to the future, the talk identifies key issues that must be confronted in furthering the quest for abstraction and automation.

Biography:

Dr Alan M Frisch is a Reader in Intelligent Systems and Head of the Artificial Intelligence Group in the Dept. of Computer Science at the Univ. of York.  He is currently a SICSA Distinguished Visiting Fellow.

For over 30 years he has been teaching artificial intelligence and researching various topics within the field, including a focus on constraint programming over the past decade.  He is an acknowledged
leader in constraint modelling, best known for his pioneering contributions in the automation of constraint modelling, in inventing the ESSENCE problem specification language, and in developing symmetry-breaking constraints.

Alan M Frisch – Artificial Intelligence Group – Department of Computer Science – University of York, UK.

Event details

  • When: 7th November 2011 14:00 - 15:00
  • Where: Phys Theatre C
  • Series: CS Colloquia Series
  • Format: Colloquium

Design, Agency and a Sense of Wellbeing by Ann Light

Abstract:

In Capability and Wellbeing, Sen (1993) says that acting freely and being able to choose may be directly conducive to wellbeing, not just because more freedom may make better alternatives available, but because the action of choice is itself a freedom. This talk reflects on three projects with older people and considers their sense of agency in thinking about interactive systems and future technologies, looking particularly at how agency might contribute to a sense of wellbeing. Although a theme running through the talk is the design of digital tools, the discussion takes a broad view of the factors to be considered in human-computer interaction.

Sen, Amartya. (1993). Capability and Well-Being. In M. Nussbaum and A. Sen, eds. The Quality of Life, pp. 30–53. New York: Oxford University Press.

Continue reading

Event details

  • When: 28th November 2011 14:00 - 15:00
  • Where: Phys Theatre C
  • Series: CS Colloquia Series
  • Format: Colloquium

Quantifying human vision: perception of depth and shape by Julie Harris

Abstract

The human visual system is extraordinary powerful, but it is not a perfect seeing device. In this talk I will use the example of binocular vision to explore visual processing. I will describe some of the biology of the binocular visual system, some of the limitations that the biology presents, and I will describe methods used to probe the relative importance of binocular vision, versus other sources of 3-D visual information. These methods allow us to predict where and when binocular vision provides a powerful source of 3-D information, and is therefore useful to inform the design and production of devices across a range of HCI applications.


Bio


Julie Harris is interested in visual perception, with particular interests in how binocular vision and eye movements are used for the perception of shape and depth and the control of action in 3-D space. Current projects include how binocular information is used for distance perception, how gaze patterns can be described in simple mathematical terms, and how we perceive motion in three dimensions.

Event details

  • When: 30th April 2012 14:00 - 15:00
  • Where: Phys Theatre C
  • Series: CS Colloquia Series
  • Format: Colloquium

ParaForming: Forming Parallel Haskell Programs using Novel Refactoring Techniques by Prof Kevin Hammond

Abstract

Despite Moore’s “law”, uniprocessor clock speeds have now stalled. Rather than using single processors running at ever higher clock speeds, it is common to find dual-, quad- or even hexa-core processors, even in consumer laptops and desktops. Future hardware will not be slightly parallel, however, as in today’s multicore systems, but will be massively parallel, with manycore and perhaps even megacore systems becoming mainstream. This means that programmers need to start thinking parallel. To achieve this they must move away from traditional programming models and development processes that offer parallelism as an bolted-on afterthought.

This talk introduces the idea of “paraforming”, a new approach to constructing parallel functional programs using formally-defined refactoring transformations.
We show how parallel programs can be built from a small number of primitive Haskell building blocks, and describe some new refactorings for Parallel Haskell that capture common parallel abstractions, such as divide-and-conquer and data parallelism using these building blocks. Using a paraforming approach, we are able to easily obtain significant and scalable speedups (up to 7.8 on an 8-core machine).

Continue reading

Event details

  • When: 21st November 2011 14:00 - 15:00
  • Where: Phys Theatre C
  • Series: CS Colloquia Series
  • Format: Colloquium

Friendlists, Followers and Contacts: Using Self-Reported Social Networks to Improve Opportunistic Networks by Gregory Bigwood

Abstract:

Opportunistic networks provide an ad hoc communication medium without the need for an infrastructure network, by leveraging human encounters and mobile devices. Routing protocols in opportunistic networks frequently rely upon encounter histories to build up meaningful data to use for informed routing decisions. This seminar presents work showing it is possible to use pre-existing social-network information to improve existing opportunistic routing protocols, and that these self-reported social networks have a particular benefit when used to bootstrap an opportunistic routing protocol.

Frequently, opportunistic routing protocols require users to relay messages on behalf of one another: an act that incurs a cost to the relaying node. Nodes may wish to avoid this forwarding cost by not relaying messages. Opportunistic networks need to incentivise participation and discourage the selfish behaviour. This seminar further presents an incentive mechanism that uses self-reported social networks to construct and maintain reputation and trust relationships between participants, and demonstrates its superior performance over existing incentive mechanisms.

Biography:

Greg Bigwood is a Ph.D. student in the School of Computer Science at the University of St Andrews. He works in the field of opportunistic networks and social networks, researching the use of social-network information to improve opportunistic networks.

He read Computer Science at the University of St Andrews, graduating in 2007.

Event details

  • When: 31st October 2011 14:00 - 15:00
  • Where: Phys Theatre C
  • Series: CS Colloquia Series
  • Format: Colloquium

Systems and Security Modelling: From Theory to Practice (Really) by Professor David J. Pym

Abstract: I describe a mathematical systems modelling framework that is motivated by a desire to represent and reason about properties of (large-scale) systems situated in dynamic environments. Motivated by the concepts of distributed systems theory, the framework has at its core mathematical treatments of environment, location, resource, and process, and comes along with a separating modal logic. Extensions to analyze questions in computer security are also considered. The mathematical structures provide a semantics for a modelling tool, called (Core) Gnosis, that, together with some elementary utility theory, has been deployed in a range of commercial projects undertaken with Hewlett-Packard’s information security business and its customers. I conclude by discussing the rôle of economics in the context of modelling questions in information security.




Biography:

Professor David J. Pym, 6th Century Chair in Logic, and SICSA Professor of Computing Science, Head of School of Natural and Computing Sciences, University of Aberdeen. Previously Principal Scientist at HP Labs, Bristol and Professor of Logic & Computation at Bath, Professor of Logic at QMUL. PhD Edinburgh; MA, ScD Cambridge; FIMA, FBCS.

Led the ‘Security Analytics’ project at HP Labs, now deployed commercially by Hewlett-Packard in its information security business. One of the designers of the Core Gnosis tool for systems and security modelling which is used to deliver the modelling part of Security Analytics. See this recent news piece about my colleagues at HP: http://www.hpl.hp.com/news/2011/oct-dec/security_analytics.html


David is currently interested in the following areas:


  • Mathematical systems modelling, using algebraic, logical, and stochastic methods, with applications in information security;
  • Topics related to the economics of information security;
  • Topics related to the economics of systems thinking;
  • Topics connecting logic (substructural, modal; process algebra) and utility theory;
  • Topics in logic related to information flow and trust domains;
  • Topics related to information security, information stewardship, and cloud computing;
  • Topics in logic related to the theory of search spaces.

Event details

  • When: 24th October 2011 14:00 - 15:00
  • Where: Phys Theatre C
  • Series: CS Colloquia Series
  • Format: Colloquium

Learning hard chart constraints for efficient context-free parsing by Brian Roark – Oregon Health & Science University

Abstract: In this talk, I’ll present some recent work in learning hard constraints for cells within a context-free parsing chart, to reduce parsing time. Each cell in the chart represents one of the O(n^2) substrings of the input string, and characteristics of each substring can be used to decide how much work to do in the associated chart cell. I’ll discuss finite-state models for tagging chart constraints on words, including methods for bounding the worst-case complexity of the parsing pipeline to quadratic or sub-quadratic in the length of the string. Empirical results will be presented for English and Chinese, achieved by constraining various high accuracy parsers.

Finally, I will present a generalization of these finite-state approaches that performs a quadratic number of classifications (one for each substring) to produce further (finer) constraints on the amount of processing within each cell. This latter approach has the nice property of being trained on maximum likelihood parses, rather than reference parses, making for a straightforward method for tuning parsing efficiency to new tasks and domains.

Continue reading

Event details

  • When: 27th September 2011 13:00 - 14:00
  • Where: Cole 1.33
  • Series: CS Colloquia Series
  • Format: Colloquium