TAPAS 2011 - September 17th 2011

Objectives

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.

Scope

The programme for TAPAS 2010 will consist of invited lectures followed by discussions.

 

    Invited Speakers

Tentative Program

09:00-09:15

Welcome
09:15-10:00 Freedom Before Commitment – A Lightweight Type System for Object Initialization. Peter Mueller.
10:00-10:30 Coffee Break
10:30-11:15 Static Analysis of JavaScript Web Applications. Anders Moeller.
11:15-12:00 Code Verification with Polyspace: an Overview. Mathias Peron.
12:00-13:30 Lunch Break
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.
15:00-15:30 Coffee Break
15:20-16:15 Discussion/Conclusions

Abstracts

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.

Static Analysis of JavaScript Web Applications

Anders Moeller, Aarhus University, Denmark

JavaScript is the main scripting language for Web browsers, but there is still little tool support available for detecting programming errors during development. This talk gives an overview of the TAJS project that aims to provide a program analysis infrastructure that can infer detailed and sound type information for JavaScript programs using abstract interpretation. The analysis is designed to support essentially the full language as defined in the ECMAScript standard, including its peculiar object model and the built-in functions. A central challenge is how to make precise and scalable dataflow analysis for the many dynamic features of JavaScript. Another obstacle is how to model the HTML pages and the browser API that all JavaScript web applications depend on.

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.

 Organizers

Saturday, September 17th, 2011

Venice, Italy

Co-located with SAS 2011

Registration

Venue: CA' DOLFIN