Compiler verification meets cross-language linking via data abstraction. - Peng Wang 048; Santiago Cuéllar; Adam Chlipala (OOPSLA, 2014)

Compositional CompCert. - Gordon Stewart 001; Lennart Beringer; Santiago Cuéllar; Andrew W. Appel (POPL, 2015)

Bringing Order to the Separation Logic Jungle. - Qinxiang Cao; Santiago Cuéllar; Andrew W. Appel (APLAS, 2017)

Concurrent Permission Machine for modular proofs of optimizing compilers with shared memory concurrency. - Santiago Cuéllar (2020)

Cheesecloth: Zero-Knowledge Proofs of Real World Vulnerabilities. - Santiago Cuéllar; Bill Harris; James Parker; Stuart Pernsteiner; Eran Tromer (USENIX Security Symposium, 2023)