In the last ten years, a wide range of static analysis tools have emerged, some of which are currently in industrial use or are well beyond the advanced prototype level. Many impressive practical results have been obtained, which allow complex properties be proved or checked in a fully or semi automatic way, even in the context of complex software developments. In parallel, the techniques to design and implement static analysis tools have improved significantly. This workshop is intended to promote discussions between specialists in all areas of program analysis and program analyzers implementation and static analysis tools users.
The programme for TAPAS 2010 will consist of invited lectures followed by discussions.
|09:15-10:00||Freedom Before Commitment – A Lightweight Type System for Object Initialization. Peter Mueller.|
|11:15-12:00||Code Verification with Polyspace: an Overview. Mathias Peron.|
|13:30-14:15||Do-it-all object invariants in VCC: data-structures, concurrency, and secrecy. Michal Moskal.|
|14:15-15:00||Challenges of Software Verification in Industry. Franjo Ivancic.|
Challenges of Software Verification in Industry
Franjo Ivancic, NEC Labs, USA
The recent rapid increase of software in embedded systems has caused system dependability issues. This talk focuses on our effort to utilize software verification inside NEC to improve the quality of software. First, we give a brief overview of the F-Soft software verification platform, which combines abstract interpretation and bounded model checking. Then, we address the practical challenges we face to utilize Varvel, an internal product based on F-Soft, on industry software. The talk concludes with a number of lessons that we have learned in this effort.
Anders Moeller, Aarhus University, Denmark
Do-it-all object invariants in VCC: data-structures, concurrency, and secrecy.
Michal Moskal, Microsoft Research, Redmond, USA
I'm going to talk about using VCC to prove functional properties of data structures, tricky concurrency primitive implementations, and even proving cryptographic secrecy, all using object invariants, with a bit of ghost code, induction and data types.
VCC is an industrial-strength verification environment for low-level concurrent systems code written in C. VCC takes a program (annotated with function contracts, state assertions, and type invariants) and attempts to prove the correctness of these annotations. VCC's verification methodology allows global two-state invariants that restrict update of shared state and enforces simple, semantic conditions sufficient for checking those global invariants modularly. VCC works by translating C, via the Boogie intermediate verification language, to verification conditions handled by the Z3 SMT solver. The environment includes tools for monitoring proof attempts and constructing partial counterexample executions for failed proofs and has been used to verify functional correctness of tens of thousands of lines of Microsoft's Hyper-V virtualization platform and of SYSGO's embedded real-time operating system PikeOS.
VCC is available with sources (for non-commercial use) at http://vcc.codeplex.com/
Freedom Before Commitment – A Lightweight Type System for Object Initialization
Peter Mueller, ETH Zurich, Switzerland
One of the main purposes of object initialization is to establish invariants such as a field being non-null or an immutable data structure containing specific values. These invariants are then implicitly assumed by the rest of the implementation, for instance, to ensure that a field may be safely dereferenced or that immutable data may be accessed concurrently. Consequently, letting an object escape from its constructor is dangerous; the escaping object might not yet satisfy its invariants, which may lead to errors in code that relies on them. Nevertheless, preventing objects entirely from escaping from their constructors is too restrictive; it is often useful to call auxiliary methods on the object under initialization or to pass it to another constructor to set up mutually-recursive structures.
This talk presents a type system that tracks which objects are fully initialized and which are still under initialization. The type system can be used to prevent objects from escaping, but also to allow safe escaping by making explicit, which objects might not yet satisfy their invariants. We designed, formalized, and implemented our type system as an extension to a non-null type system, but it is not limited to this application. Our system is conceptually simple and requires little annotation overhead; it is sound and sufficiently expressive for many common programming idioms. Therefore, we believe it to be suitable for mainstream use.
Code Verification with Polyspace: an Overview
Mathias Peron, Polyspace, Math Works, France
Since 1999, Polyspace provides a code verifier of C, C++ and ADA code, based on abstract interpretation. It aims at proving the absence of a large class of runtime errors and is meant to be used by any developer. In a first part, we will explain how Polyspace delivers the static analysis results to the user, reviewing some of our main functional design choices. We will present Polyspace's workflow, notably how we help the user to quickly detect defects, and monitor the quality of several software in time, thanks to Polyspace Metrics. Finally, we will briefly show how Polyspace is now used by Simulink to verify models. In a second part, we will give insights how Polyspace is developed and validated, an important point notably for certification. The presentation will be scattered with demos.