ICE 2012

June 16th, 2012      KTH in Stockholm (Sweden) (satellilte of DisCoTec'12) organised with Artist partners 


ICE 2012 programme

Time Slot Talk
08h55 – 9h00 Opening
09h00 – 10h00 Invited talk: Marcello Bonsangue
Conformance Testing of Interacting Components
10h00 – 10h30 Break
10h30 – 11h00 Andres Aristizabal, Filippo Bonchi, Luis Pino
and Frank Valencia
Reducing Weak to Strong Bisimilarity in CCP
11h00 – 11h30 Johannes Borgström, Ramunas Gutkovas, Joachim
Parrow, Björn Victor and Johannes Åman Pohjola
Sorted Psi-calculi with Generalised Pattern Matching
11h30 – 12h00 Etienne Lozes and Jules Villard
Shared Contract Obedient Endpoints
12h00 – 12h30 Gabriele Costa, Fabio Matinelli and
Artsiom Yautsiukhin
Metric-Aware Secure Service Orchestration
12h30 – 14h00 Lunch
14h00 – 15h00 Invited talk: Ichiro Hasuo
Nonstandard Static Analysis: Discrete Verification
Methodologies Transferred to Hybrid Applications
15h00 – 15h30 Simon Bliudze
Towards a Theory of Glue
15h30 – 16h00 Break
16h00 – 16h30 Kyriakos Poyias and Emilio Tuosto
Enforcing Architectural Styles in Presence of
Unexpected Distributed Reconfigurations
16h30 – 17h00 Dan Ghica and Zaid Al-Zobaidi
Coherent Minimisation: Towards efficient
tamper-proof compilation
17h00 – 17h30 Jurriaan Rot, Irina Mariuca Asavoae, Frank De Boer,
Marcello Bonsangue and Dorel Lucanu
Interacting via the Heap in the Presence of Recursion
17h30 – 17h40 Closing
19h00 – ... Workshop Dinner

Abstracts of Invited Talks

- Marcello Bonsangue (LIACS & CWI, The Netherlands) “Conformance Testing of Interacting Components”

In component based software engineering, distributed components interact using complex coordination patterns that may be implemented by networks of communication channels. Channels receive stimuli from the environment possibly causing interactions to take place. In this talk I will introduce an execution model for channel based coordination, and present some principles and methods for testing implementations of coordination patterns to ensure their correct responses with respect to stimuli specifications.

- Ichiro Hasuo (University of Tokyo, Japan) “Nonstandard Static Analysis: Discrete Verification Methodologies Transferred to Hybrid Applications”

*Hybrid systems* are those which exhibit both discrete "jump" and continuous "flow" dynamics. Their importance---as components of *cyber-physical systems*---is paramount now that more and more physical systems (cars, airplanes, etc.) are controlled with computers.

There are naturally two directions towards the study of hybrid systems: *control theory* (typically continuous) and *formal verification* (typically discrete). For us from the formal verification community, therefore, the big challenge is how to incorporate continuous "flow" dynamics. Many existing techniques---such as hybrid automaton or Platzer’s differential dynamic logic---include differential equations explicitly. This incurs a difficult (and very interesting) question of how to handle differential equations.

In our project we take a different path of *turning flow into jump*---more precisely into infinitely many jumps each of which is infinitesimal (i.e. infinitely small). This makes everything discrete jump dynamics, to which all the discrete techniques accumulated in the community of formal verification readily apply. This venture is mathematically supported by *nonstandard analysis*, where we can rigorously speak about infinites and infinitesimals.

In the talk I will lay out: 1) our framework of a while-language and a Hoare-style program logic, augmented with an infinitesimal constant, for modeling and verification of hybrid systems; 2) how discrete verification techniques can be *transferred*, as they are, to hybrid applications, via the celebrated *transfer principle* in nonstandard analysis; and 3) the overview of our prototype automatic prover.

The talk is based on the joint work with Kohei Suenaga, Kyoto University. References:

[1] Kohei Suenaga and Ichiro Hasuo. Programming with Infinitesimals: A While-Language for Hybrid System Modeling. Proc. ICALP 2011, Track B. LNCS 6756, p. 392-403. Springer-Verlag.

[2] Ichiro Hasuo and Kohei Suenaga. Exercises in Nonstandard Static Analysis of Hybrid Systems. To appear in Proc. CAV 2012.

(c) Artist Consortium, All Rights Reserved - 2006, 2007, 2008, 2009

Réalisation Axome - Création de sites Internet