Tony Hoare: Laws of concurrent system design
Envie de télécharger cette vidéo sur votre ordinateur ? Cliquez ici (poids : 613 Mo)
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
Orateur(s) : Tony Hoare, Microsoft Research Cambridge
Public : Tous
Date : Tuesday 26 November 2013
Lieu : Amphithéâtre Durand, Campus Jussieu
- Le temps et les événements en informatique
- Le génie mathématique, du théorème des quatre couleurs à la classification des groupes
- Unifying logic and probability: A “New Dawn” for Artificial Intelligence?
- Taking Education Online: A Unique Opportunity for the New Millenium
- Lauréat prix Gilles Kahn 2012 : Camille Couprie
- Lauréat prix Gilles Kahn 2012 : Mathilde Noual
- Lauréat prix Gilles Kahn 2012 : Mathieu Feuillet
- Gilles Dowek: Are formal methods the future of air traffic control?
- Tony Hoare: Laws of concurrent system design
- On the Preservation of Digital Information
- L'information mentale
- Myths about MOOCs and Software Engineering Education
- Toward a Theory of Trust in Networks of Humans and Computers
- Computer Science: All Questions Answered
- Fluidization of discrete event models or a marriage between the discrete and the continuous
- Vers des bases de connaissances personnelles
- The new era of biology is computational
- Proofs, Secrets, and Computation
- Desperately seeking software perfection
- Les informaticiennes, de la dominance de classe aux discriminations de sexe
- Cybersecurity and network measurement : problematic in so many ways
- Really Big Data Analytics on Graphs with Trillions of Edges
- Robots that exceed human capabilities
- "Chirps" everywhere
- Abstract interpretation
- What Makes Digital Inclusion Good Or Bad? Liste détaillée.
En savoir +
Si vous rencontrez des problèmes pour visualiser la vidéo, nous vous recommandons de mettre à jour Flash Player