18/1/2013: Registration open
18/1/2013: Abstract submissions open
5/3/2013: Deadline for booking on-campus accommodation
7/3/2013: EXTENDED!! Deadline for application for bursaries
10/3/2013: Deadline for registration
10/3/2013: Deadline for submission of abstracts
24 - 27/3/2013: Colloquium
The conference is being held in the East Building on the University of Bath campus. Maps and directions can be found at http://www.bath.ac.uk/about/gettinghere/.
Talks will be held in East Building 1.1 and refreshments will be served in the East Building foyer.
Samson Abramsky, University of Oxford.
Abstract to follow.
Extensive and expensive testing is the primary method used to gain confidence in safety-critical software today. There are some notable exceptions where formal software verification has been successfully used and scaled to large industrial projects. SPARK is a programming language, a set of verification tools, and a design approach for such critical systems. A number of military and commercial high integrity projects, ranging from 10 000 to 5 million lines of code, have been developed in SPARK. Examples include Rolls Royce Trent (engine control), EuroFighter Typhoon (military aircraft), and NATS iFACTS (air traffic control).
We have identified two reasons why formal program verification is still a hard sell: 1) the difficulty of reaching non-expert users, and 2) the lack of a convincing cost-benefit argument. In this talk I will describe our approach to solve those two problems in the design of the new SPARK 2014 language and its associated verifying compiler, developed jointly by Altran UK and AdaCore. I will give an overview of some lessons learned from the programming language and verification research community, from the development of industrial standards such as DO-178C, and from our experiences in the industrial use of SPARK. In particular I will describe our unique integration of testing and proving. We argue that subprogram level formal verification using SPARK 2014 can be cheaper than testing in DO-178C terms, and that our integrated approach allows a mix of test and proof so that the most cost-effective method can be used for each part of a program.
We study algorithmic techniques for energy savings in computer systems. We consider power-down mechanisms that transition an idle system into low power stand-by or sleep states. Moreover, we address dynamic speed scaling, a relatively recent approach to save energy in modern, variable-speed microprocessors.
In the first part of the talk we survey important results in the area of energy-efficient algorithms. In the second part we investigate a setting where a variable-speed processor is equipped with an additional sleep state. This model integrates speed scaling and power-down mechanisms. We consider classical deadline-based scheduling and settle the complexity of the offline problem. As the main contribution we present an algorithmic framework that allows us to develop a number of significantly improved constant-factor approximation algorithms.
Assia Mahboubi, INRIA - École Polytechnique.
For the last decades, computers have been playing an increasing role in the everyday activity of many researchers in mathematics: for typesetting articles, for testing conjectures, and sometimes even for validating parts of proofs by large computations. However most mathematicians are hardly familiar with "proof assistants", which are also pieces of software for "doing mathematics with a computer". These systems allow their users to trust with the highest degree of certainty the validity of the proofs they have carefully described to the machine. So far proof assistants have been successfully employed to verify the correctness of hardware and software components with respect to given specifications, scrutinizing proofs that are too long and pedestrian to be checked by hand. In September 2012, a proof of the Odd Order Theorem (Feit-Thompson, 1963), which is a milestone for the the classification of finite simple groups, was machine-checked by the Coq proof assistant. In this case, the computer has verified a proof which does not rely on heavy computations but on a sophisticated combination of mathematical theories resulting in one of the longest published proof of its time. In this talk we will give an overview of the panel of research areas and methodologies that should be combined in order to ensure the success of such a formalization. Black (or white) board will eventually never be surpassed to convey and give rise to the intuitions of the mind who discovers new mathematics, but having proofs checked by a machine rather than by a human reviewer may open some new perspectives we will discuss.