mercredi 20 novembre 2013

Tony Hoare (Sir Charles Antony Richard Hoare) en conférence in Paris

Chères et chers collègues,

C'est avec plaisir que nous vous convions à assister au prochain Colloquium
d'informatique UPMC Sorbonne Universités  


Sir Charles Antony Richard (aka Tony) Hoare
Microsoft Research Cambridge

Ce colloquium s'adresse à un public large, et est ouvert à tous les chercheurs et
étudiants en informatique. L'exposé sera en anglais. 

L'exposé aura lieu:
Mardi, 26 Novembre 2013 à 18:00

*Amphithéâtre Durand*, Université Pierre et Marie Curie     --    (attention
changement d'amphi) 
Campus de Jussieu, 4, place Jussieu, 75005 Paris
Pour y aller  :

La conférence sera diffusée en direct sur, et sera accessible en
différé, quelques jours plus tard, à partir de

Un cocktail est, en principe, prévu à 17h15, en prélude à la conférence. Il sera
confirmé par la suite. 

Ultra-short bio: Tony Hoare is one of the founders of modern informatics. He
invented pre/post-condition logic, Quicksort, monitors and CSP, and was a pioneer of
concurrent programming. He is a Fellow of the Royal Society since 1982 and was
awarded the ACM Alan Turing Prize in 1980, the Kyoto Prize in 2000, and the John von
Neumann medal in 2011.

Colloquium: Laws of concurrent system design
The algebraic laws that govern the behaviour of concurrent systems, with both
sequential and concurrent composition, are as simple as the familiar laws of
arithmetic learnt at school. They are strong enough to derive the structural rules
of Hoare logic, which were designed as a proof system for verification of programs.
They also derive the rules of O'Hearn's separation logic. They also derive the rules
of a structural operational semantics, such as those used by Milner to define
validity of an implementation of CCS. The laws are simpler than each of these
calculi separately, and stronger than both of them combined.
The laws are satisfied by a simple graph model of the behaviour of a concurrent
system, in which basic actions are nodes, connected by arrows that represent
dependency between actions. Such a graph might be produced by a testing tool to help
reveal the causes of an error, and decide what to do about it. The model is highly
generic, and can be used for systems with different basic actions, expressed in
different languages, and at different levels of granularity and abstraction.
I speculate that one day algebraic laws such as these will be accepted as a
scientific and semantic basis for a Design Automation toolkit for systems
engineering. Its tools will include system verification, program analysis, program
generation, compilation and optimisation, test case generation, and error analysis.

Tony Hoare toujours actif ! CSP, CCS, etc... nostalgie ! est-ce que nos jeunes collègues peuvent encore enseigner cela à la génération qui clique plus vite que son ombre.

Aucun commentaire:

Site Meter