Note: Detailed information about all events is also collected in the programme booklet.

Keynote Speakers

The distinguished Carl Adam Petri lecture will be given by

Sir C. A. R. (Tony) Hoare
C. A. R. Hoare - Photo
Microsoft Research, USA
Bio: Sir C. A. R. Hoare, commonly called Tony Hoare, studied philosophy and machine translation of languages at Oxford University and Moscow State University until 1959. After eight years as programmer, Chief Engineer, and Chief Scientist at Elliott Brothers, he obtained professorship for Computing Science at the Queen's University in Belfast, and joined the Programming Research Group at Oxford University in 1977. On reaching retirement age at Oxford, he went back to industry as a senior researcher with Microsoft Research in Cambridge. Tony Hoare is well known for his contributions to Computer Science. Among other results, he discovered the Quicksort algorithm, implemented the first commercial ALGOL 60 compiler, hosted the Z specification language design, and designed the CSP programming model.
Talk: Net Models of Concurrent Object Behaviour
Time: Thursday, 9:00
Slides: Net Models of Concurrent Object Behaviour

Confirmed keynote speakers are:

Alain Finkel
A. Finkel - Photo
ENS de Cachan, France
Bio: Alain Finkel is professor at the Ecole Normale Supérieure de Cachan (ENS Cachan). He is the creator of the theory of well-structured transition systems (PhD 1986 - Icalp'1987) and during the same years, he defined and studied (front) lossy channel systems, these two research topics being still quite active since 25 years. His current research interests still include the theory of well-structured transition systems and the verification of various other infinite-state systems. He wrote around 100 research papers: in particular, he participated at the LSV book "Systems and Software Verification. Model-Checking Techniques and Tools" which was, in 2001, the first undergraduate introduction to model-checking. He founded the computer science laboratory (LIFAC) at the ENS Cachan and then he co-founded the LSV computer science laboratory. He was co-chairman for the major Conferences STACS and CAV. Since few years, he decided to teach applied cognitive sciences for training to pedagogy PhD students of the ENS Cachan and professors in the Universities. He sometimes writes research papers in cognitive domains like mental imagery or cognitive automata.
Talk: The Theory of WSTS: The Case of Complete WSTS
Time: Friday, 9:00
Bart Jacobs
B. Jacobs - Photo
Radboud University Nijmegen, The Netherlands
Bio: Prof. dr. Bart Jacobs (1963) studied mathematics and philosophy at Nijmegen. He got his PhD in 1991, also at Nijmegen, in the area of theoretical computer science. He worked at universities of Cambridge (UK) and Utrecht, and at the Centre for Mathematics and Computer Science in Amsterdam. In 1996 Jacobs returned to Nijmegen on a research position of the Royal Netherlands Academy of Sciences (KNAW). Since 2002 he is full professor in the area of security and correctness of software. His work was supported by a prestigious Pionier grant of the Netherlands science foundation NWO. With his research group he has worked over the last decade on a number of societally relevant security topics such as chipcards (eg. in passports and transport), electronic voting, smart metering, road pricing and privacy. During 2005-2011 Jacobs was also parttime professor at the Technical University Eindhoven. In 2007 he served as a member of the "Korthals Altes" committe that advised on the future of the voting process in the Netherlands. In 2008 his research group attracted worldwide attention by showing severe security vulnerabilities in the Mifare Classic, the most widely used smart card. He is a member of the newly formed National Cyber Security Council that provides cabinet level advice in the Netherlands on strategic computer security matters.
Talk: Topics in Computer Security
Time: Wednesday, 15:00
Joost-Pieter Katoen
J.-P. Katoen - Photo
RWTH Aachen, Germany
Bio: Joost-Pieter Katoen leads the Software Modeling and Verification Group at RWTH Aachen University and is part-time associated to the University of Twente. His research interests include model checking, concurrency theory, formal semantics and probabilistic models. He is member of the steering committee of QEST, FORMATS, TACAS, and ETAPS (deputy chair), senior member of the ACM, and member of the IFIP WGs 1.8 and 2.2. With Christel Baier (TU Dresden), he published a comprehensive monograph on ``Principles of Model Checking" (MIT Press).
Talk: GSPNs Revisited: Simple Semantics and New Analysis Algorithms
Time: Wednesday, 9:00
Jens Sparsø
J. Sparsø - Photo
TU Denmark, Denmark
Bio: Jens Sparsø is professor at the Department of Informatics and Mathematical Modelling at the Technical University of Denmark (DTU). His research interests are in the field of computer engineering and include: application specific computing structures, low power design techniques, asynchronous circuits and systems, multi-processor systems-on-chip, and networks-on-chip. He is the co-author of the book "Principles of Asynchronous Circuit Design – A Systems Perspective" (Kluwer, 2001) – a widely used textbook in the field – and he has given a number of tutorials and invited talks on asynchronous design in academia and industry. He has been on the steering committees and technical program committees for several conferences, including the ASYNC and NOCS symposia, and in 2012 he is general chair and hosting the two events at DTU.
Talk: Networks-on-chip for real-time multi-processor systems-on-chip
Time: Thursday, 15:00

Keynote Topics

Net Models of Concurrent Object Behaviour

(Distinguished Carl Adam Petri Lecture)

by Sir C. A. R. (Tony) Hoare

The operators of concurrent programming include sequential composition, choice, synchrony, and concurrent composition. These operators are subject to algebraic laws as familiar and elegant as the laws governing the arithmetic operators which we learnt at school. The only unfamiliar law is that which relates sequential and concurrent composition: it is similar to the interchange law of category theory. The power of the algebra of concurrent programming is such as to permit purely algebraic proof of familiar programming calculi, like Hoare logic and separation logic and Jones rely/guarantee. Furthermore, the algebra can also prove the transitions of an operational semantics, like Milner's process calculus CCS.

But do the laws apply to specifications and designs of programs that run concurrently on today's multi-processor computer systems? To give an affirmative answer to this question, we define a realistic mathematical model of concurrent programming, and prove that it satisfies the laws. A program is modelled as the set of all its possible executions, in all possible environments. Choice is modelled as union of sets (only one operand is executed). Synchrony is intersection (both operands are executed, and behave the same), and refinement between programs is set inclusion (so the refined program is more deterministic).

An execution is modelled as an occurrence net, whose nodes are events that have occurred in and around the executing computer, and whose arrows represent a dependency between pairs of the events. Concurrent composition of executions is just their disjoint union: every event is evoked by exactly one of the concurrent operands. Sequential composition is similar, subject to the proviso that no event of the first operand can depend on any event of the second operand. These composition operators are lifted point-wise to sets.

Slides: Net Models of Concurrent Object Behaviour

The Theory of WSTS: The Case of Complete WSTS

by Alain Finkel

Well-structured transition systems (WSTS) are a general class of infinite-state systems where termination, boundedness and coverability are decidable, using simple algorithms that work forwards and backwards. These algorithms cannot decide more complex problems like the place-boundedness problem and the computation of the cover (the downward closer of the reachability set).

To achieve this goal, we consider complete WSTS where the set of states is a complete well ordering (with other technical but realistic hypotheses).

We will then describe a simple, conceptual forward analysis procedure for infinite-complete WSTS. This computes the so-called clover of a state. When S is the completion of a WSTS X, the clover in S is a finite description of the downward closure of the reachability set of X. We show that our procedure terminates in more cases than the generalized Karp-Miller procedure on extensions of Petri nets.

We will first provide a survey about the theory of WSTS and then we will focus on complete WSTS.

Topics in Computer Security

by Bart Jacobs

Typical of the area of computer security is the presence of a malicious attacker who is deliberately trying to undermine your system. This makes computer very hard, because the behaviour of the attacker is hard to predict. Formal approaches to security thus mainly serve to make your assumptions about your system and the attacker explicit. Via a number of case studies in computer security this point will be elaborated.

GSPNs Revisited: Simple Semantics and New Analysis Algorithms

by Joost-Pieter Katoen

This talk considers interactive Markov chains (IMCs), a natural generalization of transition systems and continuous-time Markov chains (CTMCs). We show how they can be used to provide a truly simple semantics of Generalized Stochastic Petri Nets (GSPNs). In fact, any GSPN. No restrictions on the concurrent/conflicting enabledness of immediate transitions are imposed. This contrasts with classical solutions for GSPNs which use weights. (A simple extension of IMCs also covers weights.)

We will present novel analysis algorithms for expected time and long-run average time objectives of IMCs, i.e., GSPNs. Two case studies indicate the feasibility of these analyses and show that a classical reliability analysis for confused GSPNs may lead to significant over-estimations of the true probabilities.

My key slogan will be: treat nondeterminism as is! This yields both a simple GSPN semantics and trustworthy analysis results.

Finally we show that IMCs naturally cover engineering notations like dynamic fault trees and the SAE-standardized Architecture Analysis & Design Language (AADL).

Networks-on-chip for real-time multi-processor systems-on-chip

by Jens Sparsø

Over the last decade, the network-on-chip concept has evolved from an academic research topic towards industrial take-up. Many of today's chip multi-processors (used in general purpose computing) and many of today's multi-processor system-on-chip platforms (used in application-specific embedded systems) are built around some form of intra-chip packet-switched interconnection-network. Designing a network-on-chip poses challenges in several very different areas: At the hardware level designers are concerned with issues like area, speed and power consumption of the routers and links in the network, as well as timing organization of the whole platform (synchronous, mesochronous, globally-asynchronous, locally-synchronous and asynchronous). At the system level designers are concerned with issues like programming model, memory hierarchy and perhaps guaranteeing of real-time requirements. The talk will review some of our past work in the field of networks-on-chip and the lessons learned, and discuss ongoing research specifically targeting networks-on-chip for real-time multi-processor systems.


Page last modified: 2012/07/02