Thorough static analysis of device drivers. - Thomas Ball 001; Ella Bounimova; Byron Cook; Vladimir Levin; Jakob Lichtenberg; Con McGarvey; Bohus Ondrusek; Sriram K. Rajamani; Abdullah Ustuner (EuroSys, 2006)

An Automata-Theoretic Approach to Hardware/Software Co-verification. - Juncao Li; Fei Xie; Thomas Ball 001; Vladimir Levin; Con McGarvey (FASE, 2010)

Formalizing hardware/software interface specifications. - Juncao Li; Fei Xie; Thomas Ball 001; Vladimir Levin; Con McGarvey (ASE, 2011)