| 2012 | VMCAI | Effective Synthesis of Asynchronous Systems from GR(1) Specifications. | Uri Klein, Nir Piterman, Amir Pnueli |
| 2010 | CAV | Jtlv: A Framework for Developing Verification Algorithms. | Amir Pnueli, Yaniv Sa'ar, Lenore D. Zuck |
| 2009 | FASE | Controller Synthesis from LSC Requirements. | Hillel Kugler, Cory Plock, Amir Pnueli |
| 2009 | MEMOCODE | Synthesis of programs from temporal property specifications. | Amir Pnueli, Uri Klein |
| 2008 | APSEC | Using Abstraction to Verify Arbitrary Temporal Properties. | Amir Pnueli |
| 2008 | CAV | Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses. | Ariel Cohen, Amir Pnueli, Lenore D. Zuck |
| 2008 | CAV | Discriminative Model Checking. | Peter Niebert, Doron A. Peled, Amir Pnueli |
| 2008 | FM | CoVaC: Compiler Validation by Program Analysis of the Cross-Product. | Anna Zaks, Amir Pnueli |
| 2008 | VMCAI | All You Need Is Compassion. | Amir Pnueli, Yaniv Sa'ar |
| 2007 | CAV | On Synthesizing Controllers from Bounded-Response Properties. | Oded Maler, Dejan Nickovic, Amir Pnueli |
| 2007 | DATE | Interactive presentation: Automatic hardware synthesis from specifications: a case study. | Roderick Bloem, Stefan J. Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Martin Weiglhofer |
| 2007 | FMCAD | Verifying Correctness of Transactional Memories. | Ariel Cohen, John W. O'Leary, Amir Pnueli, Mark R. Tuttle, Lenore D. Zuck |
| 2007 | OOPSLA | Synthesizing reactive systems from LSC requirements using the play-engine. | Hillel Kugler, Cory Plock, Amir Pnueli |
| 2007 | TACAS | "Don't Care" Modeling: A Logical Framework for Developing Predictive System Models. | Hillel Kugler, Amir Pnueli, Michael J. Stern, E. Jane Albert Hubbard |
| 2007 | VMCAI | Shape Analysis of Single-Parent Heaps. | Ittai Balaban, Amir Pnueli, Lenore D. Zuck |
| 2006 | FM | PSL Model Checking and Run-Time Verification Via Testers. | Amir Pnueli, Aleksandr Zaks |
| 2006 | FORTE | Liveness by Invisible Invariants. | Yi Fang, Kenneth L. McMillan, Amir Pnueli, Lenore D. Zuck |
| 2006 | ICALP | Invisible Safety of Distributed Protocols. | Ittai Balaban, Amir Pnueli, Lenore D. Zuck |
| 2006 | LICS | Faster Solutions of Rabin and Streett Games. | Nir Piterman, Amir Pnueli |
| 2006 | VMCAI | Ranking Abstraction of Recursive Programs. | Ittai Balaban, Ariel Cohen, Amir Pnueli |
| 2006 | VMCAI | Synthesis of Reactive(1) Designs. | Nir Piterman, Amir Pnueli, Yaniv Sa'ar |
| 2005 | ATVA | Ranking Abstraction as a Companion to Predicate Abstraction, . | Amir Pnueli |
| 2005 | CAV | IIV: An Invisible Invariant Verifier. | Ittai Balaban, Yi Fang, Amir Pnueli, Lenore D. Zuck |
| 2005 | CAV | TVOC: A Translation Validator for Optimizing Compilers. | Clark W. Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, Lenore D. Zuck |
| 2005 | FORTE | Ranking Abstraction as Companion to Predicate Abstraction. | Ittai Balaban, Amir Pnueli, Lenore D. Zuck |
| 2005 | TACAS | Temporal Logic for Scenario-Based Specifications. | Hillel Kugler, David Harel, Amir Pnueli, Yuan Lu, Yves Bontemps |
| 2005 | TACAS | Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems. | Amir Pnueli, Andreas Podelski, Andrey Rybalchenko |
| 2005 | VMCAI | Shape Analysis by Predicate Abstraction. | Ittai Balaban, Amir Pnueli, Lenore D. Zuck |
| 2005 | VMCAI | Abstraction for Liveness. | Amir Pnueli |
| 2004 | ATVA | Validating the Translation of an Industrial Optimizing Compiler. | I. Gordin, Raya Leviathan, Amir Pnueli |
| 2004 | CAV | Range Allocation for Separation Logic. | Muralidhar Talupur, Nishant Sinha, Ofer Strichman, Amir Pnueli |
| 2004 | FOSSACS | On Recognizable Timed Languages. | Oded Maler, Amir Pnueli |
| 2004 | TACAS | Liveness with Incomprehensible Ranking. | Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck |
| 2004 | VMCAI | Liveness with Invisible Ranking. | Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck |
| 2003 | CAV | Bridging the Gap between Fair Simulation and Trace Inclusion. | Yonit Kesten, Nir Piterman, Amir Pnueli |
| 2003 | FOSSACS | Parameterized Verification by Probabilistic Abstraction. | Tamarah Arons, Amir Pnueli, Lenore D. Zuck |
| 2003 | OOPSLA | Smart play-out. | David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli |
| 2003 | VMCAI | Model-Checking and Abstraction to the Aid of Parameterized Systems. | Amir Pnueli, Lenore D. Zuck |
| 2002 | CASES | Validating software pipelining optimizations. | Raya Leviathan, Amir Pnueli |
| 2002 | CAV | Liveness with (0, 1, infty)-Counter Abstraction. | Amir Pnueli, Jessie Xu, Lenore D. Zuck |
| 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 | EMSOFT | Embedded Systems: Challenges in Specification and Verification. | Amir Pnueli |
| 2002 | FMCAD | Smart Play-out of Behavioral Requirements. | David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli |
| 2002 | VMCAI | Automatic Verification of Probabilistic Free Choice. | Lenore D. Zuck, Amir Pnueli, Yonit Kesten |
| 2001 | CAV | Parameterized Verification with Automatically Computed Inductive Assertions. | Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Jiazhao Xu, Lenore D. Zuck |
| 2001 | PODC | Sticks and stones: a coding scheme for parameterized verification. | Amir Pnueli |
| 2001 | TACAS | Automatic Deductive Verification with Invisible Invariants. | Amir Pnueli, Sitvanit Ruah, Lenore D. Zuck |
| 2000 | CASES | Rigorous development of embedded systems. | Amir Pnueli |
| 2000 | CAV | Keynote Address: Abstraction, Composition, Symmetry, and a Little Deduction: The Remedies to State Explosion. | Amir Pnueli |
| 2000 | CAV | Liveness and Acceleration in Parameterized Verification. | Amir Pnueli, Elad Shahar |
| 2000 | TACAS | A Comparison of Two Verification Methods for Speculative Instruction Execution. | Tamarah Arons, Amir Pnueli |
| 1999 | CAV | Deciding Equality Formulas by Small Domains Instantiations. | Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel |
| 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 |
| 1999 | VLSID | Verifying Tomasulo's Algoithm by Refinement. | Tamarah Arons, Amir Pnueli |
| 1999 | RTSS | A Framework for Scheduler Synthesis. | Karine Altisen, Gregor Gler, Amir Pnueli, Joseph Sifakis, Stavros Tripakis, Sergio Yovine |
| 1998 | CADE | Deductive vs. Model-Theoretic Approaches to Formal Verification (Abstract of Invited Talk). | Amir Pnueli |
| 1998 | CONCUR | On Discretization of Delays in Timed Automata and Digital Circuits. | Eugene Asarin, Oded Maler, Amir Pnueli |
| 1998 | CONCUR | Herbrand Automata for Hardware Verification. | Werner Damm, Amir Pnueli, Sitvanit Ruah |
| 1998 | FM | Translation Validation: From DC+ to C*. | Amir Pnueli, Ofer Strichman, Michael Siegel |
| 1998 | FMCAD | Verification of Data-Insensitive CIrcuits: An In-Order-Retirement Case Study. | Amir Pnueli, Tamarah Arons |
| 1998 | ICALP | Algorithmic Verification of Linear Temporal Logic Specifications. | Yonit Kesten, Amir Pnueli, Li-on Raviv |
| 1998 | ICALP | Translation Validation for Synchronous Languages. | Amir Pnueli, Ofer Strichman, Michael Siegel |
| 1998 | MFCS | Modularization and Abstraction: The Keys to Practical Formal Verification. | Yonit Kesten, Amir Pnueli |
| 1998 | TACAS | Translation Validation. | Amir Pnueli, Michael Siegel, Eli Singerman |
| 1997 | CAV | Some Progress in the Symbolic Verification of Timed Automata. | Marius Bozga, Oded Maler, Amir Pnueli, Sergio Yovine |
| 1997 | CAV | Symbolic Model Checking with Rich ssertional Languages. | Yonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, Elad Shahar |
| 1997 | FOCS | Two Decades of Temporal Logic: Achievements and Challenges (Abstract). | Amir Pnueli |
| 1997 | PODC | Verification Engineering: A Future Profession (A. M. Turing Award Lecture). | Amir Pnueli |
| 1996 | CAV | A Platform for Combining Deductive with Algorithmic Verification. | Amir Pnueli, Elad Shahar |
| 1995 | LICS | A Complete Proof Systems for QPTL | Yonit Kesten, Amir Pnueli |
| 1995 | LICS | Once and For All | Orna Kupferman, Amir Pnueli |
| 1995 | STACS | On the Synthesis of Discrete Controllers for Timed Systems (An Extended Abstract). | Oded Maler, Amir Pnueli, Joseph Sifakis |
| 1994 | LICS | Compositional Verification of Real-Time Systems | Edward Y. Chang, Zohar Manna, Amir Pnueli |
| 1993 | CAV | A Decision Algorithm for Full Propositional Temporal Logic. | Yonit Kesten, Zohar Manna, Hugh McGuire, Amir Pnueli |
| 1993 | CAV | Reachability Analysis of Planar Multi-limear Systems. | Oded Maler, Amir Pnueli |
| 1993 | LICS | In and Out of Temporal Logic | Amir Pnueli, Lenore D. Zuck |
| 1992 | CONCUR | How Vital is Liveness? Verifying Timing Properties of Reactive and Hybrid Systems (Extended Abstract). | Amir Pnueli |
| 1992 | ICALP | Characterization of Temporal Property Classes. | Edward Y. Chang, Zohar Manna, Amir Pnueli |
| 1992 | ICALP | What Good Are Digital Clocks? | Thomas A. Henzinger, Zohar Manna, Amir Pnueli |
| 1991 | COLT | On the Learnability of Infinitary Regular Sets. | Oded Maler, Amir Pnueli |
| 1991 | LICS | Specifying and Proving Serializability in Temporal Logic | Doron A. Peled, Shmuel Katz, Amir Pnueli |
| 1991 | MFCS | On the Faithfulness of Formal Models. | Zohar Manna, Amir Pnueli |
| 1991 | POPL | Temporal Proof Methodologies for Real-time Systems. | Thomas A. Henzinger, Zohar Manna, Amir Pnueli |
| 1991 | POPL | Communication with Directed Logic Variables. | Alon Kleinman, Yael Moscowitz, Amir Pnueli, Ehud Shapiro |
| 1990 | FOCS | Tight Bounds on the Complexity of Cascaded Decomposition of Automata | Oded Maler, Amir Pnueli |
| 1990 | FOCS | Distributed Reactive Systems Are Hard to Synthesize | Amir Pnueli, Roni Rosner |
| 1990 | ICALP | Proving Partial Order Liveness Properties. | Doron A. Peled, Amir Pnueli |
| 1990 | LICS | Explicit Clock Temporal Logic | Eyal Harel, Orna Lichtenstein, Amir Pnueli |
| 1990 | PODC | A Hierarchy of Temporal Properties. | Zohar Manna, Amir Pnueli |
| 1989 | ICALP | Completing the Temporal Picture. | Zohar Manna, Amir Pnueli |
| 1989 | ICALP | On the Synthesis of an Asynchronous Reactive Module. | Amir Pnueli, Roni Rosner |
| 1989 | ICCAD | Specification and verification of VLSI systems. | Asher Wilk, Amir Pnueli |
| 1989 | POPL | On the Synthesis of a Reactive Module. | Amir Pnueli, Roni Rosner |
| 1988 | CONCUR | A Framework for the Synthesis of Reactive Modules. | Amir Pnueli, Roni Rosner |
| 1988 | ICSE | STATEMATE; A Working Environment for the Development of Complex Reactive Systems. | David Harel, Hagi Lachover, Amnon Naamad, Amir Pnueli, Michal Politi, Rivi Sherman, Aharon Shtull-Trauring |
| 1987 | LICS | On the Formal Semantics of Statecharts (Extended Abstract) | David Harel, Amir Pnueli, Jeanette P. Schmidt, Rivi Sherman |
| 1987 | PODC | A Hierarchy of Temporal Properties (Abstract). | Zohar Manna, Amir Pnueli |
| 1987 | POPL | Specification and Verification of Concurrent Programs By Forall-Automata. | Zohar Manna, Amir Pnueli |
| 1987 | STACS | Specification and Implementation of Concurrently Accessed Data Structures: An Abstract Data Type Approach. | S. Kaplan, Amir Pnueli |
| 1986 | LICS | Probabilistic Verification by Tableaux | Amir Pnueli, Lenore D. Zuck |
| 1986 | LICS | A Choppy Logic | Roni Rosner, Amir Pnueli |
| 1986 | POPL | A Really Abstract Concurrent Model and its Temporal Logic. | Howard Barringer, Ruurd Kuiper, Amir Pnueli |
| 1985 | ICALP | Linear and Branching Structures in the Semantics and Logics of Reactive Systems. | Amir Pnueli |
| 1985 | POPL | Checking That Finite State Concurrent Programs Satisfy Their Linear Specification. | Orna Lichtenstein, Amir Pnueli |
| 1984 | ICALP | A Hardware Implementation of the CSP Primitives and its Verification. | Dorit Ron, Flavia Rosemberg, Amir Pnueli |
| 1984 | PODC | Verification of Multiprocess Probabilistic Protocols. | Amir Pnueli, Lenore D. Zuck |
| 1984 | POPL | Temporal Verification of Carrier-Sense Local Area Network Protocols. | Dennis E. Shasha, Amir Pnueli, W. Ewald |
| 1984 | STOC | Now You May Compose Temporal Logic Specifications | Howard Barringer, Ruurd Kuiper, Amir Pnueli |
| 1983 | ICALP | Symmetric and Economical Solutions to the Mutual Exclusion Problem in a Distributed System (Extended Abstract). | Shimon Cohen, Daniel Lehmann, Amir Pnueli |
| 1983 | ICALP | Proving Precedence Properties: The Temporal Way. | Zohar Manna, Amir Pnueli |
| 1983 | POPL | How to Cook a Temporal Proof System for Your Pet Language. | Zohar Manna, Amir Pnueli |
| 1983 | STOC | On the Extremely Fair Treatment of Probabilistic Algorithms | Amir Pnueli |
| 1982 | POPL | Termination of Probabilistic Concurrent Programs. | Sergiu Hart, Micha Sharir, Amir Pnueli |
| 1982 | POPL | Is the Interesting Part of Process Logic Uninteresting - A Translation from PL to PDL. | Rivi Sherman, Amir Pnueli, David Harel |
| 1981 | FOCS | Propositional Dynamic Logic of Context-Free Programs | David Harel, Amir Pnueli, Jonathan Stavi |
| 1981 | ICALP | Finite Models for Deterministic Propositional Dynamic Logic. | Mordechai Ben-Ari, Joseph Y. Halpern, Amir Pnueli |
| 1981 | ICALP | Impartiality, Justice and Fairness: The Ethics of Concurrent Termination. | Daniel Lehmann, Amir Pnueli, Jonathan Stavi |
| 1981 | ICALP | Realizing an Equational Specification. | Amir Pnueli, R. Zarhi |
| 1981 | POPL | The Temporal Logic of Branching Time. | Mordechai Ben-Ari, Zohar Manna, Amir Pnueli |
| 1980 | FOCS | A Linear History Semantics for Distributed Languages (Extended Abstract) | Nissim Francez, Daniel Lehmann, Amir Pnueli |
| 1980 | POPL | On the Temporal Analysis of Fairness. | Dov M. Gabbay, Amir Pnueli, Saharon Shelah, Jonathan Stavi |
| 1980 | POPL | Synchronous Schemes and Their Decision Problems. | Zohar Manna, Amir Pnueli |
| 1979 | ICALP | The Modal Logic of Programs. | Zohar Manna, Amir Pnueli |
| 1977 | FOCS | The Temporal Logic of Programs | Amir Pnueli |
| 1977 | ICALP | Simple Programs and Their Decision Problems. | Amir Pnueli, Giora Slutzki |
| 1977 | STOC | A Complete Axiomatic System for Proving Deductions about Recursive Programs | David Harel, Amir Pnueli, Jonathan Stavi |
| 1969 | STOC | Formalization of Properties of Recursively Defined Functions | Zohar Manna, Amir Pnueli |