Lazy symbolic model checking. - Jin Yang 006; Andreas Tiemeyer (DAC, 2000)

The ForSpec Temporal Logic: A New Temporal Property-Specification Language. - Roy Armoni; Limor Fix; Alon Flaisher; Rob Gerth; Boris Ginsburg; Tomer Kanza; Avner Landver; Sela Mador-Haim; Eli Singerman; Andreas Tiemeyer; Moshe Y. Vardi; Yael Zbar (TACAS, 2002)

Enhanced Vacuity Detection in Linear Temporal Logic. - Roy Armoni; Limor Fix; Alon Flaisher; Orna Grumberg; Nir Piterman; Andreas Tiemeyer; Moshe Y. Vardi (CAV, 2003)

Formal Verification of Backward Compatibility of Microcode. - Tamarah Arons; Elad Elster; Limor Fix; Sela Mador-Haim; Michael Mishaeli; Jonathan Shalev; Eli Singerman; Andreas Tiemeyer; Moshe Y. Vardi; Lenore D. Zuck (CAV, 2005)

Deterministic Dynamic Monitors for Linear-Time Assertions. - Roy Armoni; Dmitry Korchemny; Andreas Tiemeyer; Moshe Y. Vardi; Yael Zbar (FATES/RV, 2006)

MAGENTA: transaction-based statistical micro-architectural root-cause analysis. - Gila Kamhi; Alexander Novakovsky; Andreas Tiemeyer; Adriana Wolffberg (DAC, 2009)

CREST: Hardware Formal Verification with ANSI-C Reference Specifications. - Andreas Tiemeyer; Tom Melham; Daniel Kroening; John O'Leary (CoRR, 2019)