Colloquium d'informatique UPMC Sorbonne Universités : Tony Hoare le 26/11

18 Novembre 2013

---

Catégorie : Journée d étude

---

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 :

http://www.upmc.fr/fr/universite/campus_et_sites/a_paris_et_en_idf/jussieu.html

La conférence sera diffusée en direct sur http://video.upmc.fr/direct.php?id=direct_colloquium_lip6, et sera accessible en différé, quelques jours plus tard, à partir de colloquium.lip6.fr.

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.