- 16
- Michael Weber, University of Twente, The Netherlands
11:00, Thursday, 15 May
Title: NIPS: Towards Reusable Components in Model Checking Tools
Abstract: The semantics of modelling languages are not always specified in a
precise and formal way, and their rather complex underlying models
make it a non-trivial exercise to reuse them in newly developed tools.
We report on experiments with a virtual machine-based approach for
state space generation. The virtual machine's (VM) byte-code language
is straightforwardly implementable, facilitates reuse and makes it an
adequate target for translation of higher-level languages like the
SPIN model checker's PROMELA, or even C. As added value, it provides
efficiently executable operational semantics for modelling languages.
To evaluate the benefits of the proposed approach, several tools have
been built around the VM implementation we developed, among them a
model checker for Embedded Systems software.
Biography:
Michael Weber is working as VeriGEM Post-Doc at University of Twente (NL)
in the Formal Methods and Tools group. He obtained his doctoral degree
from RWTH Aachen University (D) on parallel and distributed verification
algorithms.
His interests are scaling up model-checking algorithms to modern multi-core
computers and GRIDs, as well as I/O-efficient settings. His contributions
include development of model-checking tools for C code written for various
micro-controllers. He is also interested in the semantics of modelling
languages, in particular to provide formal semantics for the input language
of the SPIN model checker, PROMELA, and bridging the gap between action-based
process algebras and state-based formalisms. He is in close collaboration with
ParaDiSe Labs at MUNI Brno (Czech Republic) and their DiVinE model-checking toolkit, as well as INRIA Rhône-Alpes in the Dutch-French SENVA collaboration
- 15
- Dang Van Hung, Institute of Information Technology, Vietnamese Academy of Science and Technology
15:00, Wednesday, 30 April
Title: Reasoning about QoS Contracts in the Probabilistic Duration Calculus
Abstract: The notion of contract was introduced to component-based software development in order to facilitate the semantically correct composition of components. We extend the form of this notion which is based on designs to capture probabilistic requirements on execution time. We show how reasoning about such requirements can be done in an infinite-interval-based system of probabilistic duration calculus.
- 14
- Abigail Vargas, UNU-IIST
15:00, Friday, 25 April
Title: Formalising the translation from RSL to CSP
Abstract: Our aim is to exploit the FDR model checker for descriptions of
concurrent systems written in the RAISE Specification Language (RSL).
To do this we define a translation from RSL to CSPM, show that the
translation is a bisimulation, and then that various properties are
preserved by bisimulation. This allows us to infer properties of the
RSL description from the results of running FDR.
- 13
- Professor Zuohua Ding, Zhejiang Sci-Tech University
15:00, Wednesday, 23 April
Title: Detecting Program Deadlock With Ordinary Differential Equations
Abstract: The state explosion problem has bothered us for decades in the
static analysis of concurrent programs for deadlock detection.
We propose a new method that can be easily used to detect
program deadlocks in a practical way. Most importantly, it can
completely avoid the state-explosion problem. A concurrent
program can be described by a group of ordinary differential
equations, where each equation describes the program state
change. Therefore, instead of counting states as in discrete
event systems to analyze the program, we can analyze the
solutions of the equations. A program state can be measured
by a number between 0 and 1. This measure indicates the
extent to which the state can be reached when the program
executes. At any time instant, a program attributes a measure
to each state. We find that a program deadlocks if and only if
every state measure of the program approaches either 1 or 0.
Two types of deadlock models are considered in this talk: the
communication (OR) model and the resource sharing (AND)
model. All the equations can be solved by Matlab and by
inspecting the solution curves we can tell if a program
deadlocks.
- 12
- Lizeth Tapia, UNU-IIST
16:30, Friday, 11 April
Title: Model checking concurrent RSL with CSPM and FDR2
Abstract: RAISE Specification Language (RSL) is a formal specification language
that allows a wide range of specification styles (of datatypes,
functions and processes). On the other hand FDR2 is a model checker for
establishing properties of models expressed in CSPM; CSPM is the
combination of functional programming language with the CSP
process-algebra, CSPM is focused in process modelling and parallel
systems.
The aim of our project is to apply model checking techniques over
formal specifications expresed in RSL using FRD2; for which we have
developed a first version of a translator between RSL and CSPM.
In this talk we give an overview of the principal semantic and syntactic
differences of this two languages and show the strategy used to find the
respective equivalences in order to make the translation possible, then
we briefly talk about the development of the translation tool and
finally we show the use of the translator tool with some typical
concurrent examples.
- 11
- Yifeng Chen, Department of Computer Science, University of Durham
15:00, Friday, 11 April 2008
Title: Verifiers Are Programs
Abstract: This talks discusses the relation between execution and verification.
A simple imperative language with execution and verification
commands is introduced. A machine only executes execution commands
of a program, while the compiler only performs the verification
commands. Common commands in other languages can be defined as a
combination of execution and verification commands. Design of
verifiers then becomes program design using verification commands.
It is shown that type checking, abstract interpretation, modeling
checking and Hoare Logic are all special verification programs, so
are many of their combinations.
Biography:
Before Joining Durham, He was a Lecturer at Department of Computer
Science, University of Leicester between 2000 and 2004 , received a DPhil in
Computing from Balliol College, University of Oxford in 2001, worked as an RA
at Peking University in 1997 and received a BSc in Computer Science from
Peking University in 1996. His main interests lie in imperative, parallel and
object-oriented programming languages, including design, translation, static
analysis, semantics and specifications.
- 10
- WU Nan, Nanjing University
11:00, Friday, 11 April 2008
Title: Scalable Architecture of a Universal Quantum Computer with Fault
Tolerance and High Performance
Abstract: Quantum computation is a field of science and technology, combining
and drawing on the disciplines of physical science, mathematics, computer
science, and engineering. Indeed, scientists predict that within the
next 30 to
50 years there will be quantum computers. The architecture of a quantum
computer is therefore worthy of study. Today, most of the physically
implemented quantum devices can deal with only some specific problems or
algorithms. People have been trying to build a universal quantum computer,
which would be able to solve all kinds of problems on a single
architecture.
In recent years, quantum algorithms, quantum computational models and
physical quantum computers have been studied. The results of these studies
provide the necessary theoretical and experimental basis to design the
"next
generation" scalable universal quantum computer with new features such as
fault tolerance, high performance, and high-fidelity teleportation, etc.
These
features can also provide quantum operating system, quantum programming
languages and their compilers, the basis for implementation and the
platforms
for execution.
This talk presents a scalable architecture of a universal quantum computer
with fault tolerance and high performance.
Biography:
WU Nan received the B.Sc. degree in Computer Science from Nanjing
University
in 2004. He is now a PhD candidate in the Department of Computer Science
and
Technology at Nanjing University. His research interests mainly include
quantum information processing, quantum-computer architecture and
quantum programming languages.
- 9
- Matthias Weber, CARMEQ
11:00, Thursday, 20 March 2008
Title: Developing Embedded Automotive Systems
Abstract: This seminar will present an overview of the results of
a European-Union-funded project that involved car
manufacturers and suppliers, and universities. The main
result of the project has been an architectural-design
language for automotive systems. The language is broad
enough to include concepts for managing market lines,
a topic that is chosen as a focus for this talk. A
feature will be reflections on the place of Formal
Methods in realistic Software Engineering.
Biography:
Matthias Weber was an undergraduate in Computer Science
at the University of Karlsruhe and obtained his
Habilitation from the Technical University of Berlin.
After spending a decade working in Formal Methods at the
TUBerlin, he has spent a further decade working in the
German automotive industry - originally for Daimler and
more recently for CARMEQ. He and Viktor Friesen, a
colleague with a similar background but who works for
Daimler, are visiting Jeff Sanders (whom they have known
for two decades) for a fortnight.
- 8
- Zhang Yu, Macao University of Science and Technology
11:00, Friday, 29 February 2008
Title: Cryptographic logical relations -- Yet another framework for verifying security protocols
Abstract: Formal verification of cryptographic protocols has been
a very active research field for over a decade and it has
been well accepted that many security properties, e.g.,
the secrecy property, can be formalized using the notion
of contextual equivalence (a.k.a. observational equivalence)
of programs. In typed lambda-calculi, contextual
equivalence can usually be proved through a technique
called logical relations. However, applying logical relations
in the setting of protocol verification is not straightforward.
We have in particular concentrated on the dynamic key
(nonce) generation, which plays an important role in protocols
but is unfortunately detoured by informal conventions in
most models. Our work is based on the general model of
deriving logical relations for monadic types (by
Goubault-Larrecq et al.) and we propose a new categorical
model Set^{PI->} based on Stark's name creation monad.
We argue that this should be the right category for defining
cryptographic logical relations. Interestingly, this research
also leads us to an exploration of what should be the
correct definition of contextual equivalence in the framework.
We finally arrive at a definition also based on the new
category, where represent faithfully the capability of
adversaries, and we prove that our cryptographic logical
relations are sound w.r.t. the contextual equivalence.
The approach is applied to proving the correctness of the
Needham-Schroeder-Lowe protocol in the Dolev-Yao model.
As the work includes many technical details, I will make
the effort to give a general introduction to protocol
verification. In addition to introducing the formal models,
based on the framework mentioned above of course, we
shall also talk about some topics at the frontier of the field,
especially the more refined computational model where
more realistic crypto-systems are taken into account.
We will discuss on the possibility of extending our
framework to fit in the computational model.
Biography:
ZHANG Yu is an assistant professor in Macao University of Science and
Technology. He got his PhD from École Normale Supérieure de Cachan in
France in 2005. Before moving to Macao he had also been working in CEA
(the French Commissariat of Atomic Energy) and INRIA Sophia-Antipolis.
His research interest addresses essentially on the formal verification
of security protocols, using in particular logical methods from type
theory, semantics of programming languages, etc. At MUST he is
teaching two courses for the moment: Computer Architecture and
Analysis of Security Protocols.
- 7
- Fabrizio Luccio, University of Pisa, Italy
11:00, Friday, 22 February 2008
Title: A Boolean approach to transaction mining for discovering frequent itemsets (work in progress
Abstract: Managing frequent itemsets is a fundamental problem in managing large
databases of customer transactions. To ease the mining process, closed
itemsets have been defined as candidate for expressing the problem without
loss of information.
However, the number of such itemsets may be exponential in the size of the
input.
In this work we are trying to apply Boolean algebra methods for circuit
design to describe the itemset problem in a much more compact way than
the one used in current database technology. New Boolean techniques are
being developed for the present problem that might be useful also for
special circuit synthesis. Suggestions on this work are highly welcome.
Biography:
Link: Biography
- 6
- Padmanabhan Krishnan, Bond University, Australia
11:00, Monday, 18 February 2008
Title: Secure Document Circulation
Abstract: Interoperable e-business applications are essential for increasing
efficiency in the digital economy. In this talk we present an
architecture for secure document circulation designed for securing
information flow for interorganisational workflows.
We also describe the key aspects of a prototype implementation.
Slide available: slide
- 5
- Thomas Anung Basuki, UNU-IIST
11:00, Friday, 15 February 2008
Title: Model-checking Biological Systems using Calculi of Looping Sequences
Abstract: Recent advances in cell biology have made biologists realise
that a cell is a very complex system. Computer modelling can
help biologists to understand more about cell activity, behaviour
and interaction with the environment. Formal methods developed
for concurrent systems have been applied to model and reason about
cells. All formalisms that have been proposed are only partly
capable to model biological systems. Calculi of Looping Sequences
are a class of formalisms that can model both the structure of cells
and the activities occuring inside them. Stochastic CLS, a formalism
belonging to this class, supports stochastic modelling and simulation
of biological systems. However, analysing a system only through
simulation has some limitations. Not all possible behaviours of the
system can be covered by traditional simulation. These limitations can
be overcome by using model-checking, a verification technique that
performs exhaustive simulation of the system model. In this seminar
we propose an approach to model-check Calculi of Looping Sequences
models.
Slide available: slide
- 4
- Chris George, UNU-IIST
11:00, Friday, 1 February 2008
Title: An algorithmic problem: grids to shapes
Abstract: This is an informal, interactive seminar in which we look at the problem
of efficiently converting large grids (arrays of values) into polygonal
shapes. Participants are invited to consider the problem beforehand and
be ready to briefly explain their intended approach.
Slide available: Grids to shapes
- 3
- Chris George, UNU-IIST
11:00, Friday, 25 January 2008
Title: The WaterBase Project
Abstract: WaterBase is a UNU project, joint between UNU-IIST and UNU_INWEH, to
promote Integrated Water Resources Management (IWRM) in developing
countries. It aims to promote IWRM by building a network of users and
developers of a suite of modelling and decision support tools, together
with other on-line resources. The first such tool, which supports river
basin modelling, has just been released. See http://www.waterbase.org.
Slide available: WaterBase
- 2
- Stephen Ellis, NASA
11:00, Thursday, 17 January 2008
Title: Virtual environments and the examined life: or Whatever happened to VR
Abstract:
- 1
- Einar Broch Johnsen, University of Oslo
11:00, Friday 11 January 2008
Title: Modeling and Analysis in Maude
Abstract: This is an informal talk in three parts. Part one is a general
discussion about the applicability and design of (formal)
specification languages. Part two provides a high-level overview of
Maude, a freely available, modern, and widely applicable
specification language and tool. Part three gives a quick primer and
demo of the use of this language and tool. As this is an informal
talk, questions, comments, and discussions along the way will be most
welcome.
Biography:
Einar Broch Johnsen is associate professor at the University of Oslo. His
PhD (2002) was on formal viewpoint specification of open distributed
systems. In addition to object orientation and open systems, his research
interests include formal systems and methods such as rewriting logic, proof
systems, type theory, and theorem proving.