Main Page

Verifying Automatically the Correct Use and Implementation of Container Libraries

The growing need for automated services in our fast-going society demands for in- creasingly complex software artifacts. To tackle this complexity, most programming languages offer Application Programming Interfaces (API) allowing software developers to use abstract data structures (sets, maps, stacks, queues, etc.), known as containers. This project aims at defining scalable program analyses based on modular views of programs, at two levels of abstraction: (1) a high level view, in which data containers are black boxes, handled via abstract specification contracts, and (2) a low level view of the implementation of containers as recursive data structures. We plan to develop (a) decision procedures for logics able to describe complex data structures, (b) verification tools based on model checking and static analysis, and (c) techniques for automatic generation of refinement relations between specifications and implementations. We plan to carry out experiments on industrial test cases.