| 2003 | CAV | Bridging the Gap between Fair Simulation and Trace Inclusion. | Yonit Kesten, Nir Piterman, Amir Pnueli |
| 2002 | CONCUR | Network Invariants in Action. | Yonit Kesten, Amir Pnueli, Elad Shahar, Lenore D. Zuck |
| 2002 | CONCUR | A Deductive Proof System for CTL. | Amir Pnueli, Yonit Kesten |
| 2002 | VMCAI | Automatic Verification of Probabilistic Free Choice. | Lenore D. Zuck, Amir Pnueli, Yonit Kesten |
| 1999 | CSL | Verifying Liveness by Augmented Abstraction. | Yonit Kesten, Amir Pnueli |
| 1999 | FM | A Perfect Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software. | Yonit Kesten, Amit Klein, Amir Pnueli, Gil Raanan |
| 1998 | ICALP | Algorithmic Verification of Linear Temporal Logic Specifications. | Yonit Kesten, Amir Pnueli, Li-on Raviv |
| 1998 | MFCS | Modularization and Abstraction: The Keys to Practical Formal Verification. | Yonit Kesten, Amir Pnueli |
| 1997 | CAV | Symbolic Model Checking with Rich ssertional Languages. | Yonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, Elad Shahar |
| 1995 | LICS | A Complete Proof Systems for QPTL | Yonit Kesten, Amir Pnueli |
| 1993 | CAV | A Decision Algorithm for Full Propositional Temporal Logic. | Yonit Kesten, Zohar Manna, Hugh McGuire, Amir Pnueli |