A Formally-Verified Alias Analysis. - Valentin Robert; Xavier Leroy (CPP, 2012)

Automating formal proofs for reactive systems. - Daniel Ricketts 001; Valentin Robert; Dongseok Jang; Zachary Tatlock; Sorin Lerner (PLDI, 2014)

Front-end tooling for building and maintaining dependently-typed functional programs. - Valentin Robert (2018)

A type system for extracting functional specifications from memory-safe imperative programs. - Paul He; Eddy Westbrook; Brent Carmer; Chris Phifer; Valentin Robert; Karl Smeltzer; Andrei Stefanescu; Aaron Tomb; Adam Wick; Matthew Yacavone; Steve Zdancewic (Proc. ACM Program. Lang., 2021)

A Semantic Reference Model for Capturing System Development and Evaluation. - Abha Moitra; Paul Cuddihy; Kit Siu; Baoluo Meng; John Interrante; David W. Archer; Eric Mertens; Kevin Quick; Valentin Robert; Daniel Russell (ICSC, 2022)

RACK: A Semantic Model and Triplestore for Curation of Assurance Case Evidence. - Abha Moitra; Paul Cuddihy; Kit Siu; David W. Archer; Eric Mertens; Daniel Russell; Kevin Quick; Valentin Robert; Baoluo Meng (SAFECOMP Workshops, 2023)

Macaw: A Machine Code Toolbox for the Busy Binary Analyst. - Ryan G. Scott; Brett Boston; Benjamin Davis; Iavor S. Diatchki; Mike Dodds; Joe Hendrix; Daniel Matichuk; Kevin Quick; Tristan Ravitch; Valentin Robert; Benjamin Selfridge; Andrei Stefanescu; et al. (CoRR, 2024)