Tuesday April 9th:Anders MörtbergTitle:Inductive proofs in proof assistantsAbstract:Proof assistants are programs that assist with the development of formal proofs. This kind of tools can be used to prove properties of both software and hardware in order to increase the reliability of the implementation. In the talk I will show what such a tool can look like and how it can be used to prove properties of functions on inductively defined sets like natural numbers and lists.

Tuesday April 23rd:Wolfgang AhrendtTitle:Büchi automata and their application to software verificationAbstract:One of the most prominent methods in formal software verification is 'Model checking', a technique which is partly based on a certain extension of finite automata, called "Büchi automata". A Büchi automaton extends a finite automaton to infinite inputs. It accepts an infinite input sequence iff there exists a run of the automaton that visits one of the final states infinitely often. But who is interested in infinite words? We will answer that question in this lecture, showing that Büchi automata are a great example for how seemingly 'esoteric' theoretical notions have a great impact on areas they were not designed for. We will also demonstrate the very successful software verification tool SPIN, which uses Büchi automata to prove correctness of concurrent processes.

Tuesday April 30th:Martin FabianTitle:Supervisory Control Theory -- A Practical Application of Automata TheoryAbstract:What is usually known as the "Ramadge and Wonham Supervisory Control Theory", is a general framework for automatically generating a safety device known as a "supervisor" that restricts the behaviour of a given "plant" so that the joint "closed-loop" system of the supervisor interacting with the plant, fulfils a given "specification". In its original formulation the R&W SCT considered plants, specifications and supervisors modelled by formal languages, not necessarily regular. However, in subsequent work, the typical modelling formalism has been finite-state automata in different forms. For the closed-loop system to be well-defined, the supervisor must fulfil three properties that emanate from the fact that the supervisor is subordinate to the plant. The supervisor must be "controllable", "nonblocking" and "least restrictive" with respect to the plant. Controllability captures the limited power to control the plant by inhibiting generation of some events; this is a safety aspect, nothing bad should ever happen. Nonblocking is a property that guarantees progress, something good must always be possible. Minimal restrictiveness requires the supervisor to intervene as little as possible, this is an optimality criterion. The R&W SCT prove that a supervisor fulfilling these requirements always exists, and in the context of finite-state machines and regular languages, this supervisor is calculatable. The lecture will give a theoretical overview of the SCT, and show examples of supervisor calculations for different applications.

Tuesday May 14th:Aarne RantaTitle:Using grammars in compilers and translationAbstract:Compilers are programs that translate high-level programming languages to machine language. Grammars play an important role in compilers: they are used both for analysing the source language and for producing the machine code.

To illustrate how this works, the lecture will explain the complete pipeline for compiling Java code to Java Virtual Machine code, and the role of grammars in the pipeline. But we will also explore the limits of what grammars can do. Would the same methods apply to human languages, for instance, for translating English to Swedish? Is it realistic to expect that we will one day be able to communicate with computers in human language?

[top]