Dr.Søren Debois Visited Joint Research Center

On May 11, 2011, Dr.Søren Debois came to USTC-Yale joint research center and paid a two-day visit.Søren Debois got his PhD under the supervision of Lars Birkedal and Thomas Hildebrandt in 2008 at the IT University of Copenhagen, where he is currently employed as a post doc. His dissertation and subsequent research has centered on the development and application of the theory of bigraphs, notably "sortings", notions of higher-order bigraphs, notions of refinement for bigraphs, and applications of bigraphs to ubiquitous computing. He is currently very interested in understanding the interplay between programming languages, ubiquitous systems, and formal models of concurrency. During that time, Dr Søren Debois gave us a introcution to Bigraphs and had an in-depth discussion with us.

 Pro.Feng introduced Søren Debois to us

Dr.Søren Debois gave a brief talk.

Dr.Wei Wang dicussed with Dr.Søren Debois before seminar.

On May 12,Pro.Feng gave a talk about Relation reasoning about concurrent program transformation to Dr.Søren Debois and us.

 Dr.Søren Debois's talk:
Introduction to Bigraphs & Computation in Bigraphs
Bigraphs and Bigraphical Reactive Systems comprise a graphical model
of concurrency introduced by the late Robin Milner in 2001. The model
was intended both as a unifying framework for existing process
calculi, and as a first step towards reasoning about ubiquitous and
pervasive systems.
In this two-part talk, we will in the first half give an introduction
bigraphs: their motivation, theories, results, and applications,
requiring no particular background in process algebras or concurrency
theory. Then, in the second half, we present recent research on
injecting into bigraphs interaction semantics computation in a
traditional sense, thus solving an important problem in bigraph theory
first stated in 2005.
Pro.Feng's talk:
Relational Reasoning about Concurrent Program Transformation

Verifying program transformations usually requires proving that the
resulting program (the target) refines or is equivalent to the
original one (the source). Simulations and logical relations are
common techniques to prove the refinement relation. However, the
relation between individual sequential threads cannot be preserved in
general with the presence of parallel compositions, due to instruction
reordering and the different granularities of atomic operations at the
source and the target. On the other hand, the refinement relation
defined based on fully abstract semantics of concurrent programs
assumes arbitrary parallel environments, which is too strong and
cannot be satisfied by many well-known transformations.

In this talk, we propose a relational reasoning method for
compositional verification of concurrent program transformations. We
define a simulation relation between the target and the source. The
relation is parameterized with constraints of the environments that
the source and the target programs may compose with. It considers the
interference between threads and their environments, thus less
permissive than relations over sequential programs. It is
compositional with respect to parallel compositions as long as the
constraints are satisfied. Also, it does not require semantics
preservation under all possible environments, and can incorporate the
assumptions about environments made by specific program
transformations in the form of rely and guarantee conditions. We have
used this relational reasoning approach to verify the atomicity of
several fine-grained concurrent algorithms.