Informatik, TU Wien

Modular Verification of Shared-Memory Concurrent Systems Software

In this talk, I will give an overview of the main software verification research in my group right now, by my student Zvonimir Rakamaric.

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

Abstract

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.

Biography

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.

Hinweis

Tee: 14:30 Uhr in der Bibliothek E185.1, Argentinierstr. 8, 4. Stock (Mitte).