Research Buffet
Wednesday, September 5, 2012
3147 MEB
Lecture 3:40 p.m.
Zvonimir Rakamaric
University of Utah
Title: Formal Software Verification: Focus on Concurrency
Wednesday, September 5, 2012
3147 MEB
Lecture 3:40 p.m.
Zvonimir Rakamaric
University of Utah
Title: Formal Software Verification: Focus on Concurrency
Abstract
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.
John Regher
University of Utah
Title: Compilers are Wrong and What to Do About It
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.
John Regher
University of Utah
Title: Compilers are Wrong and What to Do About It
Abstract
Compilers are supposed to be correct, but they aren't. Every real compiler ships with multiple unfixed bugs that are known to cause the compiler to crash and/or generate incorrect code. This talk is about these bugs and what we can do about them.
Compilers are supposed to be correct, but they aren't. Every real compiler ships with multiple unfixed bugs that are known to cause the compiler to crash and/or generate incorrect code. This talk is about these bugs and what we can do about them.