Stephen D. Brookes est un informaticien théoricien, logicien et mathématicien, professeur à l'université Carnegie-Mellon. Il est connu pour ses contributions à la logique de séparation concurrente, qui lui ont valu l'attribution du prix Gödel 2016, avec Peter O'Hearn..
Carrière
Stephen Brookes obtient un B. A. en mathématiques à l'université d'Oxford en 1978 et obtient un Ph. D. en informatique à la même université sous la direction de C. A. R. Hoare en 1983 avec une thèse ayant pour titre . Il rejoint l'université Carnegie-Mellon à Pittsburgh, en Pennsylvanie, comme chercheur en informatique en 1981, et devient professeur titulaire en 2006Sgephen Brookes will receive Gödel Prize sur Carnegie-Mellon News..
Travaux La recherche de Stephen Brookes porte sur les modèles sémantiques pour les langages de programmation, et sur les logiques pour décrire le comportement de programmes concurrentsPage personnelle sur l’université Carnegie-Mellon.. L'objectif de ces recherches, pour lesquels il est soutenu en partie par la National Science Foundation, est d'améliorer la conception et l'analyse de programmes concurrents corrects.
Stephen Brookes a travaillé, avec Tony Hoare et sur divers aspects de la logique des communicating sequential processes, et notamment sur les modèles d'échec, qui est devenu la base du model checker FDR (Failure Divergence Refinement). Avec ses anciens étudiants Shai Geva, Denis Dancanet, Kathy Van Stone, Michel Schellekens, Stephen Brookes a travaillé sur des modèles sémantiques de langages de programmation à processus concurrents, comme wie Idealized CSP idéalisé ou Algol parallèle, et sur divers aspects de la sémantique intentionnelle.
Un apport essentiel de Stephen Brookes est d'avoir rendu possible, dans des travaux entrepris en commun avec O'Hearn, la vérification de programmes comportant la manipulation de pointeurs et la mémoire partagée concurrente. Grâce à la logigue de séparation concurrente, ils sont devenus des « problèmes résolus avec élégance et simplicité ». L'approche se fonde sur la logique de séparation pour les programmes séquentiels due à O'Hearn et John Reynolds. Les propositions initiales de O'Hearn se sont révélées inconsistantes, comme l'a montré un exemple de Reynolds. O'Hearn et Brookes ont corrigé les défauts ; les contributions de Brookes sont un nouveau modèle qui permet de démontrer de manière formelle la consistance de la logique. L'article primé par le prix Gödel est expose cette théorie , paru dans la Festschrift consacrée à John Reynolds.
Ces travaux, et l'impact qu'ils ont eu, font l'objet d'un article écrit en commun avec Peter O'Hearn paru dans les SIGACT News de 2016 ..
Notes et références
Bibliographie
Liens externes .
Catégorie:Informaticien canadien Catégorie:Personnalité canadienne de l'informatique Catégorie:Étudiant de l'université d'Oxford Catégorie:Personnalité en méthodes formelles Catégorie:Professeur à l'université Carnegie-Mellon Catégorie:Lauréat du prix Gödel