Ninth International Workshop on Automated Verification of Critical Systems

Image of Gregynog Logo for AVoCS 2009

Swansea University Computer Science, 23-25 September 2009

Invited Speakers

Ulrich Berger

Ulrich Berger: Proofs-as-programs in Computable Analysis.

Abstract

Since the work of Brouwer, Kolmogorov, Goedel, Kleene and many others we know that constructive proofs have computational meaning. In Computer Science this idea is promoted under the slogan "proofs-as-programs paradigm" (or "Curry-Howard correspondence"). I will present examples from computable analysis showing that this paradigm not only works in principle, but can be used to automatically synthesise practically relevant certified programs.

CV

Ulrich Berger is a Reader in Computer Science at Swansea University. His research areas are Domain Theory, Proof Theory and Lambda Calculus. He received his PhD from the University of Munich with a dissertation in Mathematics on "Total Objects and Sets in Domain Theory". His current research interests are Coinductive Definitions with applications to Program Extractions from Proofs in Constructive Analysis.


Christoph Lüth

Christoph Lüth: User Interfaces for Theorem Provers: Unexplored Potential or Necessary Nuisance?

Abstract

Theorem provers need to be interactive, and interactive theorem provers need user interfaces. This talk will review the state of the art and some open research questions in the field, in the hope of enticing participants of AVOCS to pick up gauntlet.

The history of these user interfaces mirrors the history of user interfaces in general: early on, text-based interfaces dominate, later replaced by graphical interaction. But what makes a good interface, in particular for a theorem prover? We will investigate this question, both from a technical and human-centred perspective, by reviewing the relevant research.

This will lead us to the open questions and challenges in this area: what are viable software architecture for user interfaces, which have been proposed, and why have they (not) been successful? Can we (and do we want to) take a hint from programming, and make use of modern integrated development environments for theorem proving? What are the attractive features of these? What are the latest trends in user interface design, and are they relevant to theorem proving? How should we visualise proofs? What do users expect from a theorem prover interface, and what can we realistically deliver?

CV

Christoph Lüth is a senior researcher and vice director of the safe and secure cognitive systems group at the German Research Centre for Artificial Intelligence (Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI) in Bremen.

His research covers the whole area of advanced software development, from theoretical foundations as found in category theory to the development of tools to construct or verify software, and applications in practical areas such as robotics. The overall theme here is how to reliably construct correct software.

He holds a PhD from the University of Edinburgh, and a Habilitation from the University of Bremen, where has been working as a lecturer (associate professor) prior to joining DFKI at the start of 2006. He has authored or co-authored over thirty peer-reviewed papers, and is currently the principal investigator in a research project funded by the federal ministry of education and research (BMBF) investigating provably safe control of automous mobile robots.