Improving static analyses of C programs with conditional predicates. - Sandrine Blazy; David Bühler; Boris Yakobowski (Sci. Comput. Program., 2016)

Structuring Abstract Interpreters Through State and Value Abstractions. - Sandrine Blazy; David Bühler; Boris Yakobowski (VMCAI, 2017)

Structuring an Abstract Interpreter through Value and State Abstractions:EVA, an Evolved Value Analysis for Frama-C. (Structurer un interpréteur abstrait au moyen d'abstractions de valeurs et d'états :Eva, une analyse de valeur évoluée pour Frama-C). - David Bühler (2017)

The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. - Patrick Baudin; François Bobot; David Bühler; Loïc Correnson; Florent Kirchner; Nikolai Kosmatov; André Maroneze; Valentin Perrelle; Virgile Prevosto; Julien Signoles; Nicky Williams (Commun. ACM, 2021)

Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis. - Mamy Razafintsialonina; David Bühler; Antoine Miné; Valentin Perrelle; Julien Signoles (ECOOP, 2025)

Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis (Artifact). - Mamy Razafintsialonina; David Bühler; Valentin Perrelle (Dagstuhl Artifacts Ser., 2025)