TU Wien Informatics

20 Years

Modular Verification of Shared-Memory Concurrent Systems Software

  • 2010-01-22

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).

Speakers

Curious about our other news? Subscribe to our news feed, calendar, or newsletter, or follow us on social media.

Note: This is one of the thousands of items we imported from the old website. We’re in the process of reviewing each and every one, but if you notice something strange about this particular one, please let us know. — Thanks!