- 3rd May 2006
- Ownership Types for Object Encapsulation (Adrian Francalanza)
Abstract:
Information hiding leads to separation of concerns and allows
modular analysis of programs, whereby a subprogram can be
reasoned about without the need to consider its program
context. Encapsulation is a natural method for attaining
information hiding in object oriented programming.
In this talk I will introduce ownership types, as a static
method for enforcing object encapsulation. I will also
consider a variant of ownership types which circumvent
problems associated with strict full encapsulation, such
as the efficient implementation of pervasive object oriented
programming constructs like iterators.
The talk is based on work done at MIT by Chandrasekhar
Boyapati and his research group.
- 26th April 2006
- Verification of SPDIs: Reachability (Gordon Pace)
Abstract:
Polygonal differential inclusion systems (SPDIs) are a sub-instance
of hybrid systems which combine discrete and continuous dynamics.
Reachability analysis is known to be undecidable for
most non-trivial subclasses of hybrid systems. Reachability in SPDIs
is, however, known to be decidable.
In this talk, I will present an overview SPDIs and the resolution of
the reachability question for such systems. This work was carried out
with Gerardo Scnneider from the University of Oslo.
- Friday 21st April 2006
- Memory Consumption Analysis of Java Smart Cards (Gerardo Schneider)
Abstract:
Memory is a scarce resource in Java smart cards. Developers and card suppliers
alike would want to make sure, at compile- or load-time, that a Java Card applet
will not overflow memory when performing dynamic class instantiations. Although
there are good solutions to the general problem, the challenge is still to produce
a static analyser that is certified and could execute on-card. I will present a
constraint-based algorithm which determines potential loops and (mutually) recursive
methods (which should be used in a very restricted way by programmers).
The algorithm operates on the bytecode of an applet and is written as a set of rules
associating one or more constraints to each bytecode instruction. The rules are
designed so that a certified analyser could be extracted from their proof of
correctness. By keeping a clear separation between the rules dealing with the
inter- and intra-procedural aspects of the analysis we are able to reduce the
space-complexity of a previous algorithm. I will also present some on-going work
on how to extend the algorithm for "open" smart cards.
- 5th April 2006
- Synchronous System Refinement Using Embedded Languages (Christine Vella)
Abstract:
Modular verification and refinement methods are important techniques
to reduce the state-explosion problem of verifying large and complex
systems. Modular verification allows a verification problem to be
decomposed into smaller manageable sub-problems, where each sub-problem
is verified individually. Refinement allows the verification of an
implementation against an abstract specification defining its legal
behaviour. To provide such techniques, we embed a simple refinement
language over SharpHDL, a structural hardware description language
embedded in C#. The new language basically consists of a set of
new construct classes that allow a user to define a circuit in two
ways: either by defining the observer that defines its legal behaviour
or by defining its actual structure. Such a structure can have its
behaviour assumed and then verified after being refined. We analyze
how the natures inherited from SharpHDL give more user-control over
the verification process, thus highlighting the various contributions
given by the embedded approach.
- 22nd March 2006
- Using Induction and Model Checking to Verify Infinite Regular Systems (Joseph Cordina)
Abstract:
When verifying systems made up of any arbitrary numbers of processes and
more specifically when verifying communication protocols over any number
of processes, one is faced with a state explosion problem. In general this
problem is obviously un-decidable. The norm is to model check systems up to
a small number of inter-communicating processes (usually two or three) and
then assume that it will work for n number of processes. This approach is
rarely applicable, apart from the fact that one has no formal proof of the
system. In this talk I will introduce the concept of Structural Induction,
a technique that allows one to make conclusion over systems of any number
of inter-communicating processes.
- 22nd March 2006
- Applying the concepts of Domain-Specific Embedded Languages (DSEL) to Metagaming (William Borg Barthet)
Abstract:
The concept of Metagaming is introduced as a way out of traditional
game-specific design by forcing developers to find generalisable solutions
or create players that can infer strategy from game rules. The combinator
library-based approach for specifying domain-specific information in an
expressive and flexible way is described. The reasons for embedding
domain-specific languages into existing development infrastructures are
explained as is the importance of compiling the DSEL into more efficient
representations for some application domains. The application of DSEL
technology to Computer Game Playing is presented as a solution to developing
systems for Metagaming.
- 15th March 2006
- Model Checking Hyperlinked Documents and the World-Wide-Web (Mark Barbara)
Abstract:
Applying the sound mathematical techniques that are included in the
term model checking is an attempt to bring some order, confidence
and certainty to the relatively chaotic world of the WWW. Due to
loose principles that govern the creation, storing and accessing
of websites on the WWW, it is hard to make any concrete statements
regarding any particular website. Nonetheless, by bringing some form
of order and accountability to such websites we can benefit more from
their use, and thus applying model checking to the web is a worthwhile
endeavor. The need to 'improve' the WWW and one's relationship with it
is not a new idea and has been discussed in detail before by scholars
such as Brusilovsky and de Alfaro. Although a lot of work has been
done regarding the improvement of the web in general, one must not
forget that in our particular case we are dealing with a slightly
different frame of reference, namely e-Learning websites. E-Learning
websites tend to differ significantly from other forms of websites on
a number of points that can be used to our advantage in applying model
checking techniques to them. Several such model checking techniques
have been developed, and while not all of them lend themselves well
to checking a structure such as the web, a variety of tools have been
developed which can serve our purposes.
- 8th March 2006
- A brief overview of SAT solvers (Sandro Spina)
Abstract:
Propostional satisfiability (SAT) addresses the problem
of deciding whether a particular Boolean formula in some
normal form has an assignment to its terms that makes the
formula true. As most of you know SAT was the first
established NP-complete problem [S.A.Cook]. The application
of SAT solvers has been ubiquitous within computer science
since the 1960s when Davis and Putnam proposed an algorithm
to verify whether a particular Boolean formula in conjunjtive
normal form (CNF) is SAT or UNSAT. Nowadays SAT solvers are
particularly usefull (and are effectively used) within the
areas of model checkeing and formal verification.
Although most people would know what a SAT solver is, only
a few really know how a SAT solver works. The aim of this
tutorial is to describe a series of different SAT solvers
in a chronological way and explain in some detail how each
of these SAT solvers work.
Interested readers are referred to
http://www.satlive.org
for an updated exposition to this subject.
- 1st March 2006
- Validation and Aspect-Oriented Programming (Karlston D'Emanuele)
Abstract:
Validation is the technique of using formal specifications as runtime
monitors over the specified system. This talk concentrates on proposing
interval temporal logic (ITL) notation for defining the monitoring
properties. An important concern in ITL monitoring is their dependency
on different parts of the system composition. Aspect-Oriented Programming
(AOP) is a concept for separation of concerns, where an aspect is a task
whose execution semantics are crosscutting between the system modules.
Using the definition of aspect, we argue that validation is an aspect
and oblivious to the system development. Hence, we show that ITL
monitoring can be considered as an external add-on to the system using
AOP techniques.
- 1st March 2006
- An Abstract Machine for the Pi-Calculus (Christian Tabone)
Abstract:
We analyse an abstract machine for pi-Calculus designed by David
Turner and we understand the details of how this machine interprets
pi-Calculus notation. We then focus on some optimisations applied
to this machine and how these make it perform even more efficiently.
We then transfer our thoughts in designing a similar machine, but
which can interact with a user. A change in the design will be
required and we point out the concepts and optimisations that will
be more likely to be useful to achieve our aim.
- 22nd February 2006
- A Fault-Tolerance proof for Distributed Consensus with Perfect Failure Detectors (Adrian Francalanza)
Abstract:
I consider a standard algorithm for solving consensus with perfect
failure detection, express it in a partial failure process calculus
and discuss how I intend to prove its correctness using fault tolerant
bisimulation techniques. One novel aspect of the proposed proof is
its division into two stages: the first stage analyses the algorithm
in a failure free setting whereas the second stage, considers the
behaviour of the algorithm in a partial failure setting. One
advantage motivating this approach is that the second stage, which
is considerably more demanding, need only be carried out if the first
stage is successful. I also discuss how the burden of constructing
witness bisimulations in this setup can be alleviated considerably
using tau-confluence up-to techniques together with a stronger notion
of structural equivalence.
- 15th February 2006
- Demystifying Monads (Gordon Pace)
Abstract:
The word monad instills fear into the unitiated,
and yet, seen from a programming perspective,
monads can be seen just as yet another design
pattern to introduce and abstract over state in
pure functional languages. Furthermore, without
monads, it is almost impossible to do interesting
(or useful) stuff in a language such as Haskell,
in which IO is encapsulated within a monad. In
this talk I will introduce monads and some of
their applications in Haskell.
|
|