Biological Data: Analysis, Visualisation and Prediction by Geoff Barton – Professor of Bioinformatics, College of Life Sciences, University of Dundee

Abstract: Modern biological research hinges on technologies that are able to generate very large and complex datasets. For example, recent advances in DNA sequencing technologies have led to global collections in the multi-petabyte range that are doubling every five months. These data require organising in a form that allows interpretation by a very large and diverse user community that are interested in everything from human health and disease, through crop and animal breeding to the understanding of ecosystems. In this talk I will first give an overview of core molecular biology concepts and some of the different types of data that are currently collected, I will then focus on work from my group in visualisation and analysis of sequence alignment data before turning to examples of prediction of properties and features from biological data.

Continue reading

Event details

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

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

Baby Fish Fry

Why has there been so much activity and excitement around the fish tank this week?

Baby Cichlids have been spotted hiding amongst the rocks. Let’s hope they grow large enough, not be eaten, when they make a bid for freedom.

Photographing the camera shy proved rather tricky. Masih finally succeeded this morning.

Proof engineering, from the Four Color to the Odd Order Theorem by Dr Georges Gonthier

Thirty five years ago computers made a dramatic debut in mathematics with the famous proof of the Four Color Theorem by Appel and Haken. Their role has been expanding recently, from computational devices to tools that can tackle deduction and proofs too complex for (most) human minds, such as the Kepler conjecture or the Classification of Finite Simple Groups.

 These new “machine” proofs entail fundamental changes in the practice of mathematics: a shift from craftsmanship, where each argument is a tribute to the ingenuity of the mathematician that perfected it, to a form of engineering where proofs are created more systematically. In addition to formal definitions and theorems, mathematical theories also contain clever, context-sensitive notations, usage conventions, and proof methods. To mechanize advanced mathematical results it is essential to capture these more informal elements, replacing informal and flexible usage conventions with rigorous interfaces, and exercise apprenticeship with precise algorithms. This can be difficult, requiring an array of techniques closer to software engineering than formal logic, but it is essential to obtaining formal proofs of graduate-level mathematics, and can give new insight as well.

 In this talk we will give several examples of such empirical formal mathematics that we have encountered in the process of mechanizing a large corpus of Combinatorics and Algebra required by the proofs of the Four Colour and Odd Order Theorem.

 Bio:Georges Gonthier is a Principal Researcher at Microsoft Research Cambridge. Dr. Gonthier has worked on the Esterel reactive programming language, techniques for the optimal computation of functional programs, the design and formal verification of a concurrent garbage collector, the join calculus model of concurrency, concurrency analysis of the Ariane 5 flight software, using full abstraction in the analysis of security properties, and a fully computer-checked proof of the famous Four Colour Theorem. He now heads the Mathematical Components project at the MSR Inria Joint Center, following up on the latter work with the development of a comprehensive library of formalized abstract algebra.

Georges Gonthier – Head of the Mathematical Components team Microsoft Research-INRIA joint centre http://www.msr-inria.inria.fr/

There will be bisquits from 3:45 downstairs

Event details

  • When: 10th November 2011 16:00 - 17:00
  • Where: Maths Theatre C
  • Format: Seminar

One from the archives: Plans for new computer science building

November 2002, and plans were unveiled in the university news, for a new Computer Science Building. Stages of the build were photographed for posterity.

Continued Success For MSc Students

Work carried out by Mary Steele, Titilayo Adegbamiye (both supervised by Gordon) and Shangyi Jiang (supervised by Ishbel), in fulfilment of their MSc, has continued success.

Mary’s dissertation focus, promoting public awareness of the links between lifestyle and cancer A controlled study of the usability of health information leaflets, has been accepted for publication in the International Journal of Medical Informatics.

Titilayo’s disssertation focus, evaluating the Usability of Home Blood Pressure Monitors, featured in Workshop Proceedings at INTERACT 2011. Final proceedings are now available.

Charlie’s (Shangyi Jiang) focus on virtual worlds contributed to Ishbel’s Paper, A taxonomy of virtual worlds usage in education, recently accepted by the British Journal of Educational Technology.