Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions. - Alexey Solovyev; Charles Jacobsen; Zvonimir Rakamaric; Ganesh Gopalakrishnan (FM, 2015)

A Parameterized Floating-Point Formalizaton in HOL Light. - Charles Jacobsen; Alexey Solovyev; Ganesh Gopalakrishnan (NSV, 2015)

Lightweight Capability Domains: Towards Decomposing the Linux Kernel. - Charles Jacobsen; Muktesh Khole; Sarah Spall; Scotty Bauer; Anton Burtsev (ACM SIGOPS Oper. Syst. Rev., 2015)

Rigorous Estimation of Floating-Point Round-Off Errors with Symbolic Taylor Expansions. - Alexey Solovyev; Marek S. Baranowski; Ian Briggs; Charles Jacobsen; Zvonimir Rakamaric; Ganesh Gopalakrishnan (ACM Trans. Program. Lang. Syst., 2019)