[Schedule page]
Tuesday April 23rd: Wolfgang Ahrendt
Tuesday April 30th: Martin Fabian
Tuesday May 14th: Aarne Ranta
[top]
Tuesday April 9th: Anders Mörtberg
Title: Inductive proofs in proof assistants
Abstract: 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.
Title: Büchi automata and their
application to software verification
Abstract: 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.
Title: Supervisory Control Theory -- A Practical
Application of Automata Theory
Abstract: 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.
Title: Using grammars in compilers and translation
Abstract: 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?