Software is large, complex, and error-prone. The trend in hardware design of switching to multi-core architectures makes software development even more complex. Cutting software development costs and ensuring higher reliability of software is of global interest and a grand challenge. Formal software verification is an important part of a spectrum of techniques for achieving that goal.
I will start this lecture by motivating the need for software verification, in particular for concurrent software verification. Then, I'll introduce the theory behind a simple software verifier that is based on a theorem prover, followed by a brief overview of the practical research I did on checking concurrent systems code. The lecture should provide you with a basic understanding of what formal software verification is and why we need it, and it will also give you a flavor of one of my research contributions in this area.
Currently, Zvonimir Rakamaric is a postdoctoral fellow at Carnegie Mellon University in Silicon Valley, where he works closely with researchers from the Robust Software Engineering Group at NASA Ames Research Center. In the spring of 2012, Zvonimir will join the School of Computing at the University of Utah as a tenure-track assistant professor. He received his Ph.D. and M.Sc. from the Department of Computer Science at the University of British Columbia, where his supervisor was Alan Hu. Zvonimir completed his undergraduate studies in Croatia at the University of Zagreb.
The main focus of Zvonimir's research is developing practical methods, techniques, and tools for improving reliability and correctness of complex systems. Currently, his emphasis is on highly automatic and scalable analysis techniques for software, in particular for concurrent software. He is interested in any technique that supports those goals, such as extended static checking, automated theorem proving, model checking, and runtime verification.
Zvonimir was the recipient of a Microsoft Research Graduate Fellowship from 2008-2010. He also won the Silver Medal in the ACM Student Research Competition at the 32nd International Conference on Software Engineering (ICSE) 2010 and the Outstanding Student Paper Award at the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2007.