| 2010 | FMCAD | A single-instance incremental SAT formulation of proof- and counterexample-based abstraction. | Niklas En, Alan Mishchenko, Nina Amla |
| 2007 | TACAS | Combining Abstraction Refinement and SAT-Based Model Checking. | Nina Amla, Kenneth L. McMillan |
| 2004 | FMCAD | A Hybrid of Counterexample-Based and Proof-Based Abstraction. | Nina Amla, Kenneth L. McMillan |
| 2003 | CONCUR | Abstract Patterns of Compositional Reasoning. | Nina Amla, E. Allen Emerson, Kedar S. Namjoshi, Richard J. Trefler |
| 2003 | TACAS | Experimental Analysis of Different Techniques for Bounded Model Checking. | Nina Amla, Robert P. Kurshan, Kenneth L. McMillan, Ricardo H. Medel |
| 2003 | TACAS | Automatic Abstraction without Counterexamples. | Kenneth L. McMillan, Nina Amla |
| 2002 | FORTE | Visual Specifications for Modular Reasoning about Asynchronous Systems. | Nina Amla, E. Allen Emerson, Kedar S. Namjoshi, Richard J. Trefler |
| 2001 | CAV | Rtdt: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams. | Nina Amla, E. Allen Emerson, Robert P. Kurshan, Kedar S. Namjoshi |
| 2001 | TACAS | Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams. | Nina Amla, E. Allen Emerson, Kedar S. Namjoshi, Richard J. Trefler |
| 2000 | FMCAD | Model Checking Synchronous Timing Diagrams. | Nina Amla, E. Allen Emerson, Robert P. Kurshan, Kedar S. Namjoshi |