Institute of Computer Languages
Compilers and Languages Group

Talks 2010 - Alan Hu

Der Arbeitsbereich für Programmiersprachen und Übersetzer am Institut für Computersprachen lädt zu folgendem Vortrag ein:

Prof. Alan Hu, Ph.D.

University of British Columbia, Vancouver, BC, Canada


Modular Verification of Shared-Memory Concurrent Systems Software

Datum: Freitag, 22. Januar 2010
Zeit: 15:00 s.t.
Ort: TU Wien, Bibliothek E185.1, Argentinierstraße 8, 4. Stock (Mitte)


In this talk, I will give an overview of the main software verification research in my group right now, by my student Zvonimir Rakamaric. Zvonimir has decided to target particularly high-value software: the low-level systems software that everything else depends on, e.g., device drivers, operating systems, virtual machine monitors, hypervisors, etc. In this domain, the soundness of the verification approach is important, and the only sound verification technique that has demonstrated sufficient scalability and precision is a modular approach (with manual annotations of pre-conditions, post-conditions, loop invariants, etc.). Unfortunately, a modular approach has many problems dealing with systems software, and our research has been a step-by-step attack on these problems. Results so far are: reducing the effort of annotation by automating the generation of most frame axioms; developing a flexible memory model that accurately handles type-unsafe, low-level code, yet is still scalable; and an approach to analyze (bounded context swap) low-level, concurrent software. Zvonimir's tools have discovered several real bugs in real software, and he is currently doing an internship at Microsoft Research with the goal of further, practical applications of his tools.

Kurzbiographie von Prof. Alan Hu, Ph.D.

Alan J. Hu received his BS and PhD degrees from Stanford University. He is a Professor and former Associate Head in the Computer Science Department at the University of British Columbia. For nearly 20 years, his main research focus has been automated, practical techniques for formal verification. He has served on the program committees of all major CAD and formal verification conferences, and chaired or co-chaired CAV (1998), HLDVT (2003), FMCAD (2004), and HVC (2008). He was also a Technical Working Group Key Contributor on the 2001 International Technology Roadmap for Semiconductors, and is a member of the Technical Advisory Board of Jasper Design Automation. ( )

Sie möchten auf diesen Vortrag durch Aushang hinweisen? Eine druckfertige Einladung im pdf-Format dafür finden Sie hier.

   About Us
      Talks 2017
      Talks 2016
      Talks 2015
      Talks 2014
      Talks 2013
      Talks 2012
      Talks 2011
      Talks 2010
      Talks 2009
      Talks 2008
      Talks 2007
      Talks 2006
      Talks 2005
      Talks 2004
Fast Access:
Previous Talk
Next Talk
Faculty of Informatics
Vienna University of Technology
top | HTML 4.01 | last update: 2017-02-13 (Webmaster)