Open-Source Model Checking. - Radu Grosu; Xiaowan Huang; Sumit Jain; Scott A. Smolka (SoftMC@CAV, 2005)

Compiler-assisted software verification using plug-ins. - Sean Callanan; Radu Grosu; Xiaowan Huang; Scott A. Smolka; Erez Zadok (IPDPS, 2006)

Deep Random Search for Efficient Model Checking of Timed Automata. - Radu Grosu; Xiaowan Huang; Scott A. Smolka; Wenkai Tan; Stavros Tripakis (Monterey Workshop, 2006)

Dynamic Path Reduction for Software Model Checking. - Zijiang Yang 006; Bashar Al-Rawi; Karem A. Sakallah; Xiaowan Huang; Scott A. Smolka; Radu Grosu (IFM, 2009)

Using Integer Clocks to Verify the Timing-Sync Sensor Network Protocol. - Xiaowan Huang; Anu Singh; Scott A. Smolka (NASA Formal Methods, 2010)

Aspect-Oriented Instrumentation with GCC. - Justin Seyster; Ketan Dixit; Xiaowan Huang; Radu Grosu; Klaus Havelund; Scott A. Smolka; Scott D. Stoller; Erez Zadok (RV, 2010)

Using integer clocks to verify clock-synchronization protocols. - Xiaowan Huang; Anu Singh; Scott A. Smolka (Innov. Syst. Softw. Eng., 2011)

InterAspect: aspect-oriented instrumentation with GCC. - Justin Seyster; Ketan Dixit; Xiaowan Huang; Radu Grosu; Klaus Havelund; Scott A. Smolka; Scott D. Stoller; Erez Zadok (Formal Methods Syst. Des., 2012)

Software monitoring with controllable overhead. - Xiaowan Huang; Justin Seyster; Sean Callanan; Ketan Dixit; Radu Grosu; Scott A. Smolka; Scott D. Stoller; Erez Zadok (Int. J. Softw. Tools Technol. Transf., 2012)