Invited Talks:
Thomas Ball Microsoft Research, Redmond, USA
On the Design and Implementation of Static Analysis Tools
At Microsoft, we now regularly apply a new generation of static analysis tools that can automatically identify serious defects in programs. These tools examine millions of lines of code every day, long before the software is released for general use. With these tools, we catch more defects earlier in the software process, enabling Microsoft to deliver more reliable systems. A number of these tools have been released for general use through Microsoft's Visual Studio integrated development environment as well as freely available development kits.
In this talk I will address the question: "How does one design and implement a static analysis tool chain to help people effectively address a software reliability problem?" In particular, I will identify a set of basic techniques that have proven very useful in constructing static analysis tools and have shown their worth through numerous applications. Experience with these techniques suggests we are approaching an exciting time when more people can contribute to the design and implementation of static analysis tools.
Jim Woodcock University of York, UK
The POSIX pilot project and the Verification Grand Challenge
We present results from the second pilot project in the Verification Grand Challenge: a formally verified specification of a POSIX-compliant file store using the Z/Eves theorem prover. The project's overall objective is to build a verified file store for space-flight missions. Our specification of the file store is based on Morgan and Sufrin's specification of the UNIX filing system; the proof and its mechanisation in Z/Eves are novel. We show how our work contributes towards building a verified software repository: a set of general theories and experiments reusable across different domains.
Sérgio Campos Universidade Federal de Minas Gerais, Brazil
Bioinformatics: Genomics, Proteomics and Systems Biology
Bioinformatics has become popular with the development of several genome projects. These projects have been made possible with the advent of automatic sequencers that have allowed scientists to map complete genome of several organisms, including humans. But in spite of the large quantity of data generated by these projects, it is still not clear what they mean for science or for society. This is a challenge that bioinformatics as a research area has to tackle. This talk presents a "systemic" view of bioinformatics, a perspective about research in this area starting with genomics (represented by the genome projects) and ending with systems biology, which represents the integration of the main methodologies and results in a single area. A path is proposed to understand not only what to do with the large amounts of biological data generated so far, but also to where bioinformatics is headed, with a vision of the types of problems, tools and expected results that bioinformatics will be dealing with in the future.
Tutorial: Thomas Ball Microsoft Research, Redmond, USA
HAVOC: Heap Aware Verifier for C programs using SMT solvers
In this tutorial, we will present a framework for modular, automatic and precise verification for C programs. We will illustrate how to provide an operational semantics for C programs by providing a memory model that accounts for the various features of C including dynamic casts, deallocation, nested structures, internal pointers, address arithmetic, arrays, that are frequently present in systems software (operating systems, device drivers). Given the memory model, we show how we translate a C program to a BoogiePL program, a simple intermediate language with clear semantics. We will briefly describe how to generate a verification condition, a logical formula that characterizes the correctness of the BoogiePL program.
We will next discuss an annotation language for specifying pre-conditions, post-conditions and loop invariants for the C programs. The annotation language is expressive enough to state interesting properties of the heap related to unbounded recursive data structures like linked lists and deeply nested structures. The annotation language also provides concise ways to express non-aliasing of various data structures. Unlike prior attempts of using first-order solvers, our annotation language makes systematic use of quantifiers, which allows us to automate the proofs of the verification conditions. We will illustrate the underlying logic that is used to express these annotations and briefly discuss the prover for the logic. Finally, we will illustrate the application of the tool on a set of small to medium sized C benchmarks taken from custom storage allocators, device drivers, and other applications.
Reference: http://research.microsoft.com/~shuvendu/papers/havoc_tacas07.pdf
| Organization | Scientific Sponsorship | Sponsors |
  |
    |
 
|