On-the-fly Abstract Debugging for Frama-C/Eva
This program is tentative and subject to change.
This paper introduces the Eva Abstract Debugger, a tool based on the Frama-C/Eva abstract interpreter that adapts familiar debugging paradigms—stepping, breakpoints, and state inspection—to an abstract execution, allowing users to precisely follow how the analysis runs, and monitor where precision loss occurs. We describe the tool’s architecture, which adopts a client/server approach, using the well known Debug Adapter Protocol (DAP). The client is a VS Code extension, while the server builds upon the core Eva engine. Finally, we present actions that are specific to abstract debugging, notably the ability to interactively change the precision settings to recover precision at crucial program points, or to select on-the-fly the order in which the different branches of a program are explored.
This program is tentative and subject to change.
Mon 29 JunDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
11:00 - 12:30 | |||
11:00 30mTalk | How Developers Perceive Differential Debugging: an Exploratory Survey DEBT Rémi Dufloer Univ. Lille, Inria, CNRS, Centrale Lille, UMR 9189 CRIStAL, F-59000 Lille, France, Imen Sayar Univ. Lille, CNRS, Inria, Centrale Lille, UMR 9189 CRIStAL, F-59000 Lille, France, Steven Costiou INRIA Lille, Anne Etien University of Lille, Lille, France | ||
11:30 20mTalk | On-the-fly Abstract Debugging for Frama-C/Eva DEBT Jules Massart Independent Researcher, Michele Alberti Université Paris-Saclay, CEA, List, David Bühler Université Paris-Saclay, CEA, List, Virgile Prevosto Université Paris-Saclay, CEA, List | ||
11:50 20mTalk | Wasmito: A Lightweight Framework for Building Dynamic Tools on Microcontrollers DEBT Carlos Rojas Castillo Vrije Universiteit Brussel, Matteo Marra Nokia Bell Labs, Belgium, Elisa Gonzalez Boix Vrije Universiteit Brussel | ||