Algorithms for Ordinal Arithmetic. - Panagiotis Manolios; Daron Vroon 001 (CADE, 2003)

Integrating Reasoning About Ordinal Arithmetic into ACL2. - Panagiotis Manolios; Daron Vroon 001 (FMCAD, 2004)

Ordinal Arithmetic: Algorithms and Mechanization. - Panagiotis Manolios; Daron Vroon 001 (J. Autom. Reason., 2005)

Termination Analysis with Calling Context Graphs. - Panagiotis Manolios; Daron Vroon 001 (CAV, 2006)

Automatic memory reductions for RTL model verification. - Panagiotis Manolios; Sudarshan K. Srinivasan; Daron Vroon 001 (ICCAD, 2006)

Integrating static analysis and general-purpose theorem proving for termination analysis. - Panagiotis Manolios; Daron Vroon 001 (ICSE, 2006)

Verification Condition Generation Via Theorem Proving. - John Matthews; J Strother Moore; Sandip Ray; Daron Vroon 001 (LPAR, 2006)

ACL2s: "The ACL2 Sedan". - Peter C. Dillinger; Panagiotis Manolios; Daron Vroon 001; J Strother Moore (UITP@FLoC, 2006)

BAT: The Bit-Level Analysis Tool. - Panagiotis Manolios; Sudarshan K. Srinivasan; Daron Vroon 001 (CAV, 2007)

Automating component-based system assembly. - Panagiotis Manolios; Daron Vroon 001; Gayatri Subramanian (ISSTA, 2007)

Efficient Circuit to CNF Conversion. - Panagiotis Manolios; Daron Vroon 001 (SAT, 2007)

Automatically Proving the Termination of Functional Programs. - Daron Vroon 001 (2007)

Efficient execution in an automated reasoning environment. - David A. Greve; Matt Kaufmann; Panagiotis Manolios; J Strother Moore; Sandip Ray; José-Luis Ruiz-Reina; Rob Sumners; Daron Vroon 001; Matthew Wilding (J. Funct. Program., 2008)

Faster SAT solving with better CNF generation. - Benjamin Chambers; Panagiotis Manolios; Daron Vroon 001 (DATE, 2009)

Interactive Termination Proofs Using Termination Cores. - Panagiotis Manolios; Daron Vroon 001 (ITP, 2010)

The ACL2 Sedan Theorem Proving System. - Harsh Raju Chamarthi; Peter C. Dillinger; Panagiotis Manolios; Daron Vroon 001 (TACAS, 2011)