Timed and Hybrid Statecharts and Their Textual Representation. - Yonit Kesten; Amir Pnueli (FTRTFT, 1992)

Integration Graphs: A Class of Decidable Hybrid Systems. - Yonit Kesten; Amir Pnueli; Joseph Sifakis; Sergio Yovine (Hybrid Systems, 1992)

A Decision Algorithm for Full Propositional Temporal Logic. - Yonit Kesten; Zohar Manna; Hugh McGuire; Amir Pnueli (CAV, 1993)

Temporal Verification of Simulation and Refinement. - Yonit Kesten; Zohar Manna; Amir Pnueli (REX School/Symposium, 1993)

Verifying Clocked Transition Systems. - Yonit Kesten; Zohar Manna; Amir Pnueli (Hybrid Systems, 1995)

A Complete Proof Systems for QPTL - Yonit Kesten; Amir Pnueli (LICS, 1995)

Symbolic Model Checking with Rich ssertional Languages. - Yonit Kesten; Oded Maler; Monica Marcus; Amir Pnueli; Elad Shahar (CAV, 1997)

Algorithmic Verification of Linear Temporal Logic Specifications. - Yonit Kesten; Amir Pnueli; Li-on Raviv (ICALP, 1998)

Modularization and Abstraction: The Keys to Practical Formal Verification. - Yonit Kesten; Amir Pnueli (MFCS, 1998)

Verifying Liveness by Augmented Abstraction. - Yonit Kesten; Amir Pnueli (CSL, 1999)

A Perfect Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software. - Yonit Kesten; Amit Klein 001; Amir Pnueli; Gil Raanan (World Congress on Formal Methods, 1999)

Decidable Integration Graphs. - Yonit Kesten; Amir Pnueli; Joseph Sifakis; Sergio Yovine (Inf. Comput., 1999)

Verification of Clocked and Hybrid Systems. - Yonit Kesten; Zohar Manna; Amir Pnueli (Acta Informatica, 2000)

Verification by Augmented Finitary Abstraction. - Yonit Kesten; Amir Pnueli (Inf. Comput., 2000)

Control and Data Abstraction: The Cornerstones of Practical Formal Verification. - Yonit Kesten; Amir Pnueli (Int. J. Softw. Tools Technol. Transf., 2000)

Verification by Augmented Abstraction: The Automata-Theoretic View. - Yonit Kesten; Amir Pnueli; Moshe Y. Vardi (J. Comput. Syst. Sci., 2001)

Symbolic model checking with rich assertional languages. - Yonit Kesten; Oded Maler; Monica Marcus; Amir Pnueli; Elad Shahar (Theor. Comput. Sci., 2001)

Network Invariants in Action. - Yonit Kesten; Amir Pnueli; Elad Shahar; Lenore D. Zuck (CONCUR, 2002)

A Deductive Proof System for CTL. - Amir Pnueli; Yonit Kesten (CONCUR, 2002)

Automatic Verification of Probabilistic Free Choice. - Lenore D. Zuck; Amir Pnueli; Yonit Kesten (VMCAI, 2002)

Complete Proof System for QPTL. - Yonit Kesten; Amir Pnueli (J. Log. Comput., 2002)

Bridging the gap between fair simulation and trace inclusion. - Yonit Kesten; Nir Piterman; Amir Pnueli (Inf. Comput., 2005)

A compositional approach to CTL* verification. - Yonit Kesten; Amir Pnueli (Theor. Comput. Sci., 2005)

Model Checking with Strong Fairness. - Yonit Kesten; Amir Pnueli; Li-on Raviv; Elad Shahar (Formal Methods Syst. Des., 2006)