Helmut Veith

informaticien autrichien

Helmut Veith () est un informaticien autrichien qui a travaillé dans les domaines du model checking, génie logiciel, sécurité des systèmes d'information, et logique pour l'informatique. Il était professeur d'informatique à l'université technique de Vienne (TU Wien)[2],[1],[3],[4].

Biographie

modifier

Helmut Veith obtient le titre de Diplom-Ingenieur en logique informatique à la TU Wien en 1994. En 1998, il obtient un doctorat en informatique sur la complexité des logiques et des langages de requête dans les bases de données[5] avec une thèse préparée sous la supervision de Georg Gottlob intitulée « Succinct Representation and the Complexity of Logics and Database Query Languages » et soutenue avec la mention « sub auspiciis praesidentis ». En 2001, il obtient l'habilitation, toujours à la TU Wien. De 2001 à 2003, Veith est professeur associé à la TU Wien, de 2003 à 2008 professeur à la université technique de Munich, de 2008 à 2009 à l'université de technologie de Darmstadt et ensuite à la TU Wien. Il était également professeur associé à l'université Carnegie-Mellon, à Pittsburgh.

Recherche

modifier

Helmut Veith est surtout connu pour sa participation dans le développement de la méthode dite « Counterexample-guided Abstraction Refinement » (CEGAR) qui est un ingrédient-clé dans les model checkers modernes, en logiciel et en matériel. Cette recherche applique des méthodes formelles et logiques aux problèmes en technologie et ingénierie du logiciel, avec en particulier le model checking, la vérification et le test de logiciels, le logiciel embarqué et la sécurité des ordinateurs. Helmut Veith a activement publié[6] en informatique, dans ces domaines de vérification assistée par ordinateur, analyse de programmes, la logique en informatique, le software engineering, et la sécurité des systèmes d'information. Il est coéditeur du Handbook of Model Checking[7] paru après sa mort.

Honneurs et distinctions

modifier

Veith est récipiendaire, avec ses sept coauteurs Edmund M. Clarke, Orna Grumberg, Ronald H. Hardin, Somesh Jha, Yuan Lu, Robert P. Kurshan et Zvi Harel, du prix CAV Award 2015 « pour le développement et l'implémentation de la technique de localisation-réduction et la formulation du raffinement de l'abstraction guidée par contre-exemple »[8],[9]. Il a aussi reçu le ACM Distinguished Paper Award « pour sa contribution à l'étude de la vérification modulaire »[10],[11]. En 2016, Veith s'est vu attribuer un ERC Advanced Grant sur le thème Harnessing Model Checking Technology for Distributed Algorithms.

Notes et références

modifier
  1. a et b « Helmut Veith », sur Google Scholar (consulté le )
  2. Page de Helmut Veith sur le site Forsyte de la TU Wien.
  3. Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu et Helmut Veith, « Counterexample-guided abstraction refinement », dans Computer Aided Verification (CAV) 2000, coll. « Lecture Notes in Computer Science » (no 1855), (DOI 10.1007/10722167_15), p. 154–169.
  4. « Nachruf auf Helmut Veith: Ein unlogischer Tod », .
  5. (en) « Helmut Veith », sur le site du Mathematics Genealogy Project
  6. « Helmut Veith », sur DBLP (consulté le )
  7. Edmund Clarke, Thomas Henzinger et Helmut Veith, Handbook of model checking, Springer, , 2017e éd. (ISBN 978-3-319-10575-8, présentation en ligne)
  8. « Réciepiendaires du prix CAV ».
  9. « CAV Award », sur International Conference on Computer-Aided Verification (consulté le )
  10. « ACM SIGSOFT Distinguished Paper Award », sur SIGSOFT (consulté le )
  11. Sagar Chaki, Edmund Clarke, Alex Groce, Somesh Jha et Helmut Veith, « Modular Verification of Software Components in C », IEEE Transactions on Software Engineering, vol. 30, no 6,‎ , p. 388–402 (DOI 10.1109/TSE.2004.22, CiteSeerx 10.1.1.5.9973)

Liens externes

modifier