Validation of assembler programs for dsps: a static analyzer

Digital Signal Processors are widely used in critical embed-ded systems to pilot low-level, often critical functionalities. We describe a static analyzer based on abstract interpreta-tion and designed to validate industrial assembler programs for a DSP. The validation consists of guaranteeing the ab-sence of runtime errors such as incorrect memory accesses and of tracking the sources of inaccuracies introduced by floating-point computations. Our first contribution is a new static analysis for relocatable assembler programs able to cope with dynamically computed branching addresses. Our second contribution is the analyzer itself and its graphical interface which helps the user to understand the numerical inaccuracies