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 withthe goal of further, practical applications of his tools.

Kurzbiographie von Prof. Alan Hu:

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