Working Seminar on Formal Models, Discrete Structures, and Algorithms

Combined Numerical Analysis of C Programs

Marek Trtík (Verimag)

When: December 15, 2:00pm

Where: room C417


A promising approach to checking of program properties is to combine existing analyses into a better one ideally comprising the union of strengths and the intersection of weaknesses of individual techniques. Unfortunately, the approach is difficult in general as different analyses use different formalisms and build different models of an analysed program. We focus on combining program analyses computing static program semantics in numerical domains like intervals, octagons, or convex polyhedrons. We tackle the issue how to combine such analyses without writing a code specific to them (i.e. avoiding the issue of reduced product) and we also show how to naturally represent pointers in their numerical domains in order to analyse C programs without writing a dedicated points-to or pointer-aliasing analysis.