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.

Réalisation Axome - Création de sites Internet