Obavijest o predavanju

Sažetak:

Nowadays, software is everywhere. We have software running on our personal
computers, mobile phones, in cars, ATMs, banks, planes, space shuttles, and
hospitals. Software systems are generally large, complex, and prone to
errors. According to a 2002 study by the U.S. National Institute of
Standards and Technology, software bugs are costing the U.S. economy alone
an estimated $59.5 billion each year. More importantly, there is also a
number of examples where a software error resulted in a loss of human lives.
Therefore, ensuring high reliability of software is a grand challenge and a
rapidly growing area of research.
Many approaches to software verification (i.e. debugging software) are
currently semi-automatic: a human must provide key logical insights, like
for instance procedure specifications in the form of pre- and
postconditions, assertions, etc. In the first part of the talk, I am going
to introduce a tool I have been implementing - a modular, specification
based verifier of C programs. Currently, my research is focused on
developing techniques for inferring as much as possible of the
specifications, traditionally provided manually by a user, automatically. In
the second part of the talk, I'll describe a novel technique for
automatically inferring important parts of the specifications using static
analysis. The algorithm infers so called "frame axioms" which limit the
scope of changes on the heap that must be analyzed for each procedure. The
technique builds on a pointer analysis that generates limited information
about all data structures in the heap. Our technique uses that information
to over-approximate a potentially unbounded set of memory locations modified
by each procedure/loop; this overapproximation is a candidate frame axiom. I
demonstrated the effectiveness of the approach on a number of
buffer-overflow benchmarks.

Paper on this topic can be found at
http://www.cs.ubc.ca/~zrakamar/publications/ase2008-rh.pdf

O predavaču:

Zvonimir Rakamarić is a PhD student at the University of British Columbia.
His research interests include topics in software verification and analysis.
Zvonimir's M.Sc. thesis was on verification of heap-manipulating programs,
and since then he has been working on a modular, precise, specification
based verification tool for systems code. More specifically, he is
developing novel techniques for automatizing and improving modular software
verification using static analysis. Zvonimir holds a M.Sc. degree in
computer science from the University of British Columbia and a Dipl.Ing.
degree in computer science from the Faculty of Electrical Engineering and
Computing at the University of Zagreb. Zvonimir has received the 2008
Microsoft Research Fellowship. For more information about Zvonimir, visit
www.rakamaric.com.