Funded PhD (3 years) in Program Analysis
Static Analysis and Refinement of Dynamic Data Structures
Most programming languages offer Application Programming Interfaces (API) providing ready-to-use abstract data structures (e.g. sets, maps, stacks, queues, etc.).These API’s, are known under the name of containers or collections, and provide off-the-shelf libraries of high level operations, such as insertion, deletion and membership checks. Container libraries are indeed available in almost all languages. These libraries give software developpers a way of abstracting from low-level implementation details related to memory management, such as dynamic allocation, deletion and pointer handling. However, the implementations of these libraries use optimized low-level datastructures and algorithms for heap memory management (e.g. skip lists, red-back trees, or overlaid linked lists). To ensure correctness of software systems manipulating complexdata structures, two essential issues must be considered: (1) the correctness of programs implementing applications, assuming high level specifications of the methods provided by the external container libraries they use, and (2) the correctness of the implementations of such libraries with respect to their abstract specifications, i.e., the fact that a specific implementation of containers refines the expected abstract behaviour.
The main aim of the PhD is to develop static analysis techniques which are able to prove the point (2) above. For this, the candidate will consider recent works [1] that propose abstract interpretation techniques to build abstract interpreters which are able to soundly infer properties for a logic in a generic way, if this logic satisfy some constraints (decidability of satisfiability and effectiveness of model construction). These constraints are satisfied by a large set of logics (Presburger [1], first order logic over words of integers [2], separation logic [2], tree-valued logic [1], etc.). A crucial point in this approach is the definition of suitable logic-based specification formalisms which has also an efficient symbolic representation. Indeed, such a logic is used both to specify and to reason about sets of program states (i.e. configurations of its memory) and relations between these states. The logics studied must be investigated from the point of view ofexpressive power, decidability, and complexity, by considering several key problems that constitute the basic ingredients of any automated verification approach, such as encoding of the program statements, satisfiability, and entailment checking. In general, specifying complex memory configurations requires the use of expressive formalisms (for describing shapeand data constraints), based for instance on Separation Logic with Recursive Definitions (SL+RD) or First-Order Logic with Transitive Closure (FOL+TC), for which the decidabilityof the problems mentioned above does not hold in general. The challenge is therefore to identify logics offering good trade-offs between expressiveness, decidability and complexity, and allowing to deal with significant and practically relevant classes of programs and specifications. This theoretical study will be validated by the implementation of prototype tools for static analysis of C programs (mainly based on Frama-C [3]) and decision procedures for the logics proposed.
[1] T. Reps and A. Thakur, Automating Abstract Interpretation, VMCAI'16
[2] A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu, On Inter-Procedural Analysis of Programs with Lists and Data, PLDI'11.
[3] frama-c.com
Students interested in this topic and in the position should send a CV and a letter of motivation with detailed list of competencies to Mihaela Sighireanu (mihaela DOT sighireanu AT liafa DOT unit-paris-diderot DOT fr) before June 15th, 2016.
The requested background is in theoretical computer science (logics, automata, algorithmic and complexity). Students with basic knowledge in verification, static analysis and compilation are strongly encouraged to apply. Good knowledge of at least one programming language is an asset.
