List DILS vous invite à son événement

Séminaire LSL - Jules Massart - Frama-C/Eva as a debugger engine through the Debug Adapter Protocol (DAP)

À propos de cet événement

Abstract

The Eva Abstract Debugger is an interactive tool built on top of the Eva plugin in Frama-C. It provides a debugger-like interface, integrated as a VSCode extension, to help developers explore static analysis results more intuitively. The tool allows users to step through abstract execution, inspect variable domains, set and manage breakpoints, and explore multiple abstract states when needed. Features like branch selection at conditionals and support for adding annotations on the fly aim to make static analysis more practical and accessible.

To support dynamic branch selection, the tool replaces the traditional Weak Topological Order (WTO) with a new iteration strategy based on a Weak Partial Order (WPO). This generalizes Bourdoncle’s algorithm by allowing a partial, rather than total, ordering of nodes. While currently used to control the order in which branches are explored, this approach could be extended in the future to enable parallel exploration of branches using multiple threads, improving analysis speed.

The goal is to assist users in better understanding the possible behaviors of their programs through static analysis.

Proposé par

  • Intervenant externe
    JM I
    Jules Massart

List DILS

Le CEA est un organisme de recherche sur la défense et la sécurité, les énergies nucléaire et renouvelables, la recherche technologique pour l’industrie et la recherche fondamentale en sciences de la matière et de la vie.