Amir Pnueli

Eugene Asarin, Venkatesh Mysore, Amir Pnueli, Gerardo Schneider: Low dimensional hybrid systems - decidable, undecidable, don't know. Inf. Comput. 211: 138-159 (2012)

Ittai Balaban, Amir Pnueli, Yaniv Sa'ar, Lenore D. Zuck: Verification of multi-linked heaps. J. Comput. Syst. Sci. 78(3): 853-876 (2012)

Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Yaniv Sa'ar: Synthesis of Reactive(1) designs. J. Comput. Syst. Sci. 78(3): 911-938 (2012)

Orna Kupferman, Amir Pnueli, Moshe Y. Vardi: Once and for all. J. Comput. Syst. Sci. 78(3): 981-996 (2012)

Uri Klein, Nir Piterman, Amir Pnueli: Effective Synthesis of Asynchronous Systems from GR(1) Specifications. VMCAI 2012: 283-298

Werner Damm, Henning Dierks, Jens Oehlerking, Amir Pnueli: Towards Component Based Design of Hybrid Systems: Safety and Stability. Essays in Memory of Amir Pnueli 2010: 96-143

Ittai Balaban, Amir Pnueli, Lenore D. Zuck: Proving the Refuted: Symbolic Model Checkers as Proof Generators. Concurrency, Compositionality, and Correctness 2010: 221-236

Zohar Manna, Amir Pnueli: Temporal Verification of Reactive Systems: Response. Essays in Memory of Amir Pnueli 2010: 279-361

Amir Pnueli, Yaniv Sa'ar, Lenore D. Zuck: Jtlv: A Framework for Developing Verification Algorithms. CAV 2010: 171-174

Uri Klein, Amir Pnueli: Revisiting Synthesis of GR(1) Specifications. Haifa Verification Conference 2010: 161-181

Amir Pnueli, Irina Virbitskaite, Andrei Voronkov (Eds.): Perspectives of Systems Informatics, 7th International Andrei Ershov Memorial Conference, PSI 2009, Novosibirsk, Russia, June 15-19, 2009. Revised Papers. Lecture Notes in Computer Science 5947, Springer 2010, isbn 978-3-642-11485-4

Hillel Kugler, Cory Plock, Amir Pnueli: Controller Synthesis from LSC Requirements. FASE 2009: 79-93

Amir Pnueli, Uri Klein: Synthesis of programs from temporal property specifications. MEMOCODE 2009: 1-7

Dov M. Gabbay, Amir Pnueli: A Sound and Complete Deductive System for CTL* Verification. Logic Journal of the IGPL 16(6): 499-536 (2008)

Amir Pnueli: Using Abstraction to Verify Arbitrary Temporal Properties. APSEC 2008: 3

Oded Maler, Dejan Nickovic, Amir Pnueli: Checking Temporal Properties of Discrete, Timed and Continuous Behaviors. Pillars of Computer Science 2008: 475-505

Ariel Cohen, Amir Pnueli, Lenore D. Zuck: Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses. CAV 2008: 121-134

Peter Niebert, Doron Peled, Amir Pnueli: Discriminative Model Checking. CAV 2008: 504-516

Anna Zaks, Amir Pnueli: CoVaC: Compiler Validation by Program Analysis of the Cross-Product. FM 2008: 35-51

Anna Zaks, Amir Pnueli: Program analysis for compiler validation. PASTE 2008: 1-7

Amir Pnueli, Aleksandr Zaks: On the Merits of Temporal Testers. 25 Years of Model Checking 2008: 172-195

Amir Pnueli, Yaniv Sa'ar: All You Need Is Compassion. VMCAI 2008: 233-247

Roderick Bloem, Stefan J. Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Martin Weiglhofer: Specify, Compile, Run: Hardware from PSL. Electr. Notes Theor. Comput. Sci. 190(4): 3-16 (2007)

Ittai Balaban, Amir Pnueli, Lenore D. Zuck: Modular Ranking Abstraction. Int. J. Found. Comput. Sci. 18(1): 5-44 (2007)

Oded Maler, Dejan Nickovic, Amir Pnueli: On Synthesizing Controllers from Bounded-Response Properties. CAV 2007: 95-107

Roderick Bloem, Stefan J. Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Martin Weiglhofer: Interactive presentation: Automatic hardware synthesis from specifications: a case study. DATE 2007: 1188-1193

Ariel Cohen, John W. O'Leary, Amir Pnueli, Mark R. Tuttle, Lenore D. Zuck: Verifying Correctness of Transactional Memories. FMCAD 2007: 37-44

Hillel Kugler, Cory Plock, Amir Pnueli: Synthesizing reactive systems from LSC requirements using the play-engine. OOPSLA Companion 2007: 801-802

Hillel Kugler, Amir Pnueli, Michael J. Stern, E. Jane Albert Hubbard: "Don't Care" Modeling: A Logical Framework for Developing Predictive System Models. TACAS 2007: 343-357

Ittai Balaban, Amir Pnueli, Lenore D. Zuck: Shape Analysis of Single-Parent Heaps. VMCAI 2007: 91-105

Amir Pnueli, Ofer Strichman: Reduced Functional Consistency of Uninterpreted Functions. Electr. Notes Theor. Comput. Sci. 144(2): 53-65 (2006)

Amir Pnueli, Aleksandr Zaks, Lenore D. Zuck: Monitoring Interfaces for Faults. Electr. Notes Theor. Comput. Sci. 144(4): 73-89 (2006)

Yonit Kesten, Amir Pnueli, Li-on Raviv, Elad Shahar: Model Checking with Strong Fairness. Formal Methods in System Design 28(1): 57-84 (2006)

Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck: Liveness with invisible ranking. STTT 8(3): 261-279 (2006)

Amir Pnueli, Aleksandr Zaks: PSL Model Checking and Run-Time Verification Via Testers. FM 2006: 573-586

Oded Maler, Dejan Nickovic, Amir Pnueli: From MITL to Timed Automata. FORMATS 2006: 274-289

Yi Fang, Kenneth L. McMillan, Amir Pnueli, Lenore D. Zuck: Liveness by Invisible Invariants. FORTE 2006: 356-371

Ittai Balaban, Amir Pnueli, Lenore D. Zuck: Invisible Safety of Distributed Protocols. ICALP (2) 2006: 528-539

Nir Piterman, Amir Pnueli: Faster Solutions of Rabin and Streett Games. LICS 2006: 275-284

Ittai Balaban, Ariel Cohen, Amir Pnueli: Ranking Abstraction of Recursive Programs. VMCAI 2006: 267-281

Nir Piterman, Amir Pnueli, Yaniv Sa'ar: Synthesis of Reactive(1) Designs. VMCAI 2006: 364-380

Ying Hu, Clark W. Barrett, Benjamin Goldberg, Amir Pnueli: Validating More Loop Optimizations. Electr. Notes Theor. Comput. Sci. 141(2): 69-84 (2005)

Lenore D. Zuck, Amir Pnueli, Benjamin Goldberg, Clark W. Barrett, Yi Fang, Ying Hu: Translation and Run-Time Validation of Loop Transformations. Formal Methods in System Design 27(3): 335-360 (2005)

Yonit Kesten, Nir Piterman, Amir Pnueli: Bridging the gap between fair simulation and trace inclusion. Inf. Comput. 200(1): 35-61 (2005)

Werner Damm, Bernhard Josko, Amir Pnueli, Anjelika Votintseva: A discrete-time UML semantics for concurrency and communication in safety-critical applications. Sci. Comput. Program. 55(1-3): 81-115 (2005)

Yonit Kesten, Amir Pnueli: A compositional approach to CTL* verification. Theor. Comput. Sci. 331(2-3): 397-428 (2005)

Amir Pnueli: Ranking Abstraction as a Companion to Predicate Abstraction, . ATVA 2005: 1

David Harel, Hillel Kugler, Amir Pnueli: Synthesis Revisited: Generating Statechart Models from Scenario-Based Requirements. Formal Methods in Software and Systems Modeling 2005: 309-324

Amir Pnueli: Verification of Procedural Programs. We Will Show Them! (2) 2005: 543-590

Clark W. Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, Lenore D. Zuck: TVOC: A Translation Validator for Optimizing Compilers. CAV 2005: 291-295

Ittai Balaban, Yi Fang, Amir Pnueli, Lenore D. Zuck: IIV: An Invisible Invariant Verifier. CAV 2005: 408-412

Oded Maler, Dejan Nickovic, Amir Pnueli: Real Time Temporal Logic: Past, Present, Future. FORMATS 2005: 2-16

Ittai Balaban, Amir Pnueli, Lenore D. Zuck: Ranking Abstraction as Companion to Predicate Abstraction. FORTE 2005: 1-12

Venkatesh Mysore, Amir Pnueli: Refining the Undecidability Frontier of Hybrid Automata. FSTTCS 2005: 261-272

Amir Pnueli, Andreas Podelski, Andrey Rybalchenko: Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems. TACAS 2005: 124-139

Hillel Kugler, David Harel, Amir Pnueli, Yuan Lu, Yves Bontemps: Temporal Logic for Scenario-Based Specifications. TACAS 2005: 445-460

Amir Pnueli: Abstraction for Liveness. VMCAI 2005: 146-146

Ittai Balaban, Amir Pnueli, Lenore D. Zuck: Shape Analysis by Predicate Abstraction. VMCAI 2005: 164-180

Lenore D. Zuck, Amir Pnueli: Model checking and abstraction to the aid of parameterized systems (a survey). Computer Languages, Systems & Structures 30(3-4): 139-169 (2004)

I. Gordin, Raya Leviathan, Amir Pnueli: Validating the Translation of an Industrial Optimizing Compiler. ATVA 2004: 230-247

Muralidhar Talupur, Nishant Sinha, Ofer Strichman, Amir Pnueli: Range Allocation for Separation Logic. CAV 2004: 148-161

Oded Maler, Amir Pnueli: On Recognizable Timed Languages. FoSSaCS 2004: 348-362

David Harel, Hillel Kugler, Amir Pnueli: Smart Play-Out Extended: Time and Forbidden Elements. QSIC 2004: 2-10

Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck: Liveness with Incomprehensible Ranking. TACAS 2004: 482-496

Tamarah Arons, Jozef Hooman, Hillel Kugler, Amir Pnueli, Mark van der Zwaag: Deductive Verification of UML Models in TLPVS. UML 2004: 335-349

Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck: Liveness with Invisible Ranking. VMCAI 2004: 223-238

Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel: Erratum ("The small model property: how small can it be?" Volume 178, Number 1 [2002], pages 279-293). Inf. Comput. 184(1): 227 (2003)

Lenore D. Zuck, Amir Pnueli, Benjamin Goldberg: VOC: A Methodology for the Translation Validation of OptimizingCompilers. J. UCS 9(3): 223-247 (2003)

Amir Pnueli, Tamarah Arons: TLPVS: A PVS-Based LTL Verification System. Verification: Theory and Practice 2003: 598-625

Yonit Kesten, Nir Piterman, Amir Pnueli: Bridging the Gap between Fair Simulation and Trace Inclusion. CAV 2003: 381-393

Michael Langberg, Amir Pnueli, Yoav Rodeh: The ROBDD Size of Simple CNF Formulas. CHARME 2003: 363-377

Na'aman Kam, David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli, E. Jane Albert Hubbard, Michael J. Stern: Formal Modeling of C. elegans Development: A Scenario-Based Approach. CMSB 2003: 4-20

Tamarah Arons, Amir Pnueli, Lenore D. Zuck: Parameterized Verification by Probabilistic Abstraction. FoSSaCS 2003: 87-102

David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli: Smart play-out. OOPSLA Companion 2003: 68-69

Amir Pnueli, Lenore D. Zuck: Model-Checking and Abstraction to the Aid of Parameterized Systems. VMCAI 2003: 4

Oded Maler, Amir Pnueli (Eds.): Hybrid Systems: Computation and Control, 6th International Workshop, HSCC 2003 Prague, Czech Republic, April 3-5, 2003, Proceedings. Lecture Notes in Computer Science 2623, Springer 2003, isbn 3-540-00913-2

Allen Leung, Krishna V. Palem, Amir Pnueli: TimeC: A Time Constraint Language for ILP Processor Compilation. Constraints 7(2): 75-115 (2002)

Lenore D. Zuck, Amir Pnueli, Yi Fang, Benjamin Goldberg: VOC: A Translation Validator for Optimizing Compilers. Electr. Notes Theor. Comput. Sci. 65(2): 2-18 (2002)

Lenore D. Zuck, Amir Pnueli, Yi Fang, Benjamin Goldberg, Ying Hu: Translation and Run-Time Validation of Optimized Code. Electr. Notes Theor. Comput. Sci. 70(4): 179-200 (2002)

Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel: The Small Model Property: How Small Can It Be? Inf. Comput. 178(1): 279-293 (2002)

Yonit Kesten, Amir Pnueli: Complete Proof System for QPTL. J. Log. Comput. 12(5): 701-745 (2002)

Raya Leviathan, Amir Pnueli: Validating software pipelining optimizations. CASES 2002: 280-287

Amir Pnueli, Jessie Xu, Lenore D. Zuck: Liveness with (0, 1, infty)-Counter Abstraction. CAV 2002: 107-122

Amir Pnueli, Yonit Kesten: A Deductive Proof System for CTL. CONCUR 2002: 24-40

Yonit Kesten, Amir Pnueli, Elad Shahar, Lenore D. Zuck: Network Invariants in Action. CONCUR 2002: 101-115

Amir Pnueli: Embedded Systems: Challenges in Specification and Verification. EMSOFT 2002: 1-14

David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli: Smart Play-out of Behavioral Requirements. FMCAD 2002: 378-398

Werner Damm, Bernhard Josko, Amir Pnueli, Anjelika Votintseva: Understanding UML: A Formal Semantics of Concurrency and Communication in Real-Time UML. FMCO 2002: 71-98

Amir Pnueli: Applications of Formal Methods in Biology. FTRTFT 2002: 81-82

Lenore D. Zuck, Amir Pnueli, Yonit Kesten: Automatic Verification of Probabilistic Free Choice. VMCAI 2002: 208-224

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

Yonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, Elad Shahar: Symbolic model checking with rich assertional languages. Theor. Comput. Sci. 256(1-2): 93-112 (2001)

Allen Leung, Krishna V. Palem, Amir Pnueli: Scheduling time-constrained instructions on pipelined processors. ACM Trans. Program. Lang. Syst. 23(1): 73-103 (2001)

Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Jiazhao Xu, Lenore D. Zuck: Parameterized Verification with Automatically Computed Inductive Assertions. CAV 2001: 221-234

Dana Fisman, Amir Pnueli: Beyond Regular Model Checking. FSTTCS 2001: 156-170

Doron Peled, Amir Pnueli, Lenore D. Zuck: From Falsification to Verification. FSTTCS 2001: 292-304

Amir Pnueli, Yoav Rodeh, Ofer Strichman: Range Allocation for Equivalence Logic. FSTTCS 2001: 317-333

Amir Pnueli: Sticks and stones: a coding scheme for parameterized verification. PODC 2001: 14

Amir Pnueli, Sitvanit Ruah, Lenore D. Zuck: Automatic Deductive Verification with Invisible Invariants. TACAS 2001: 82-97

Yonit Kesten, Zohar Manna, Amir Pnueli: Verification of Clocked and Hybrid Systems. Acta Inf. 36(11): 837-912 (2000)

Yonit Kesten, Amir Pnueli: Verification by Augmented Finitary Abstraction. Inf. Comput. 163(1): 203-243 (2000)

Orna Lichtenstein, Amir Pnueli: Propositional Temporal Logics: Decidability and Completeness. Logic Journal of the IGPL 8(1): 55-85 (2000)

Yonit Kesten, Amir Pnueli: Control and Data Abstraction: The Cornerstones of Practical Formal Verification. STTT 2(4): 328-342 (2000)

Amir Pnueli: Rigorous development of embedded systems. CASES 2000: 1

Amir Pnueli: Keynote Address: Abstraction, Composition, Symmetry, and a Little Deduction: The Remedies to State Explosion. CAV 2000: 1

Amir Pnueli, Elad Shahar: Liveness and Acceleration in Parameterized Verification. CAV 2000: 328-343

Ekaterina Sedletsky, Amir Pnueli, Mordechai Ben-Ari: Formal Verification of the Ricart-Agrawala Algorithm. FSTTCS 2000: 325-335

Tamarah Arons, Amir Pnueli: A Comparison of Two Verification Methods for Speculative Instruction Execution. TACAS 2000: 487-502

Bengt Jonsson, Amir Pnueli, Camilla Rump: Proving Refinement Using Transduction. Distributed Computing 12(2-3): 129-149 (1999)

Yonit Kesten, Amir Pnueli, Joseph Sifakis, Sergio Yovine: Decidable Integration Graphs. Inf. Comput. 150(2): 209-243 (1999)

Amir Pnueli, Ofer Strichman, Michael Siegel: Translation Validation: From SIGNAL to C. Correct System Design 1999: 231-255

Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel: Deciding Equality Formulas by Small Domains Instantiations. CAV 1999: 455-469

Yonit Kesten, Amir Pnueli: Verifying Liveness by Augmented Abstraction. CSL 1999: 141-156

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

Olivier Bournez, Oded Maler, Amir Pnueli: Orthogonal Polyhedra: Representation and Computation. HSCC 1999: 46-60

Karine Altisen, Gregor Gößler, Amir Pnueli, Joseph Sifakis, Stavros Tripakis, Sergio Yovine: A Framework for Scheduler Synthesis. RTSS 1999: 154-163

Tamarah Arons, Amir Pnueli: Verifying Tomasulo's Algoithm by Refinement. VLSI Design 1999: 306-309

Amir Pnueli, Ofer Strichman, Michael Siegel: The Code Validation Tool CVT: Automatic Verification of a Compilation Process. STTT 2(2): 192-201 (1998)

Allen Leung, Krishna V. Palem, Amir Pnueli: A Fast Algorithm for Scheduling Time-Constrained Instructions on Processors with ILP. IEEE PACT 1998: 158-

Amir Pnueli: Deductive vs. Model-Theoretic Approaches to Formal Verification (Abstract of Invited Talk). CADE 1998: 301

Werner Damm, Amir Pnueli, Sitvanit Ruah: Herbrand Automata for Hardware Verification. CONCUR 1998: 67-83

Eugene Asarin, Oded Maler, Amir Pnueli: On Discretization of Delays in Timed Automata and Digital Circuits. CONCUR 1998: 470-484

Amir Pnueli, Ofer Strichman, Michael Siegel: Translation Validation: From DC+ to C*. FM-Trends 1998: 137-150

Amir Pnueli, Tamarah Arons: Verification of Data-Insensitive CIrcuits: An In-Order-Retirement Case Study. FMCAD 1998: 351-368

Amir Pnueli, Natarajan Shankar, Eli Singerman: Fair Synchronous Transition Systems and Their Liveness Proofs. FTRTFT 1998: 198-209

Yonit Kesten, Amir Pnueli, Li-on Raviv: Algorithmic Verification of Linear Temporal Logic Specifications. ICALP 1998: 1-16

Amir Pnueli, Ofer Strichman, Michael Siegel: Translation Validation for Synchronous Languages. ICALP 1998: 235-246

Yonit Kesten, Amir Pnueli: Modularization and Abstraction: The Keys to Practical Formal Verification. MFCS 1998: 54-71

Amir Pnueli, Michael Siegel, Eli Singerman: Translation Validation. TACAS 1998: 151-166

Willem P. de Roever, Hans Langmaack, Amir Pnueli (Eds.): Compositionality: The Significant Difference, International Symposium, COMPOS'97, Bad Malente, Germany, September 8-12, 1997. Revised Lectures. Lecture Notes in Computer Science 1536, Springer 1998, isbn 3-540-65493-3

Marius Bozga, Oded Maler, Amir Pnueli, Sergio Yovine: Some Progress in the Symbolic Verification of Timed Automata. CAV 1997: 179-190

Yonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, Elad Shahar: Symbolic Model Checking with Rich ssertional Languages. CAV 1997: 424-435

Werner Damm, Amir Pnueli: Verifying out-of-order executions. CHARME 1997: 23-47

Werner Damm, Bernhard Josko, Hardi Hungar, Amir Pnueli: A Compositional Real-Time Semantics of STATEMATE Designs. COMPOS 1997: 186-238

Amir Pnueli: Two Decades of Temporal Logic: Achievements and Challenges (Abstract). FOCS 1997: 78

Amir Pnueli: Verifying Liveness Properties of Reactive Systems (Tutorial Abstract). HART 1997: 1

Eugene Asarin, Marius Bozga, Alain Kerbrat, Oded Maler, Amir Pnueli, Anne Rasse: Data-Structures for the Verification of Timed Automata. HART 1997: 346-360

Amir Pnueli: Verification Engineering: A Future Profession (A. M. Turing Award Lecture). PODC 1997: 7

Monica Marcus, Amir Pnueli: Using Ghost Variables to Prove Refinement. AMAST 1996: 226-240

Amir Pnueli, Elad Shahar: A Platform for Combining Deductive with Algorithmic Verification. CAV 1996: 184-195

Yonit Kesten, Zohar Manna, Amir Pnueli: Verification of Clocked and Hybrid Systems. European Educational Forum: School on Embedded Systems 1996: 4-73

Zohar Manna, Amir Pnueli: Temporal verification of reactive systems - safety. Springer 1995, isbn 978-0-387-94459-3, pp. I-XV, 1-512

Oded Maler, Amir Pnueli: On the Learnability of Infinitary Regular Sets. Inf. Comput. 118(2): 316-326 (1995)

Eugene Asarin, Oded Maler, Amir Pnueli: Reachability Analysis of Dynamical Systems Having Piecewise-Constant Derivatives. Theor. Comput. Sci. 138(1): 35-65 (1995)

Oded Maler, Amir Pnueli: Timing analysis of asynchronous circuits using timed automata. CHARME 1995: 189-205

Yonit Kesten, Zohar Manna, Amir Pnueli: Verifying Clocked Transition Systems. Hybrid Systems 1995: 13-40

Yonit Kesten, Amir Pnueli: A Complete Proof Systems for QPTL. LICS 1995: 2-12

Orna Kupferman, Amir Pnueli: Once and For All. LICS 1995: 25-35

Oded Maler, Amir Pnueli, Joseph Sifakis: On the Synthesis of Discrete Controllers for Timed Systems (An Extended Abstract). STACS 1995: 229-242

Thomas A. Henzinger, Zohar Manna, Amir Pnueli: Temporal Proof Methodologies for Timed Transition Systems. Inf. Comput. 112(2): 273-337 (1994)

Doron Peled, Amir Pnueli: Proving Partial Order Properties. Theor. Comput. Sci. 126(2): 143-182 (1994)

Amir Pnueli: Development of Hybrid Systems. FTRTFT 1994: 77-85

Arjun Kapur, Thomas A. Henzinger, Zohar Manna, Amir Pnueli: Prooving Safety Properties of Hybrid Systems. FTRTFT 1994: 431-454

Eugene Asarin, Oded Maler, Amir Pnueli: Symbolic Controller Synthesis for Discrete and Timed Systems. Hybrid Systems 1994: 1-20

Edward Y. Chang, Zohar Manna, Amir Pnueli: Compositional Verification of Real-Time Systems. LICS 1994: 458-465

Zohar Manna, Amir Pnueli: Temporal Verification Diagrams. TACS 1994: 726-765

Zohar Manna, Amir Pnueli: Models for Reactivity. Acta Inf. 30(7): 609-678 (1993)

Amir Pnueli, Lenore D. Zuck: Probabilistic Verification. Inf. Comput. 103(1): 1-29 (1993)

Yonit Kesten, Zohar Manna, Hugh McGuire, Amir Pnueli: A Decision Algorithm for Full Propositional Temporal Logic. CAV 1993: 97-109

Oded Maler, Amir Pnueli: Reachability Analysis of Planar Multi-limear Systems. CAV 1993: 194-209

Amir Pnueli, Lenore D. Zuck: In and Out of Temporal Logic. LICS 1993: 124-135

Yonit Kesten, Zohar Manna, Amir Pnueli: Temporal Verification of Simulation and Refinement. REX School/Symposium 1993: 273-346

Zohar Manna, Amir Pnueli: The temporal logic of reactive and concurrent systems - specification. Springer 1992, isbn 978-3-540-97664-6, pp. I-XIV, 1-427

Amir Pnueli: How Vital is Liveness? Verifying Timing Properties of Reactive and Hybrid Systems (Extended Abstract). CONCUR 1992: 162-175

Amir Pnueli: System Specification and Refinement in Temporal Logic. FSTTCS 1992: 1-38

Yonit Kesten, Amir Pnueli: Timed and Hybrid Statecharts and Their Textual Representation. FTRTFT 1992: 591-620

Zohar Manna, Amir Pnueli: Verifying Hybrid Systems. Hybrid Systems 1992: 4-35

Thomas A. Henzinger, Zohar Manna, Amir Pnueli: Towards Refining Temporal Specifications into Hybrid Systems. Hybrid Systems 1992: 60-76

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

Edward Y. Chang, Zohar Manna, Amir Pnueli: Characterization of Temporal Property Classes. ICALP 1992: 474-486

Thomas A. Henzinger, Zohar Manna, Amir Pnueli: What Good Are Digital Clocks? ICALP 1992: 545-558

Zohar Manna, Amir Pnueli: Time for Concurrency. 25th Anniversary of INRIA 1992: 129-153

Zohar Manna, Amir Pnueli: Completing the Temporal Picture. Theor. Comput. Sci. 83(1): 91-130 (1991)

Oded Maler, Amir Pnueli: On the Learnability of Infinitary Regular Sets. COLT 1991: 128-136

Doron Peled, Shmuel Katz, Amir Pnueli: Specifying and Proving Serializability in Temporal Logic. LICS 1991: 232-244

Zohar Manna, Amir Pnueli: On the Faithfulness of Formal Models. MFCS 1991: 28-42

Alon Kleinman, Yael Moscowitz, Amir Pnueli, Ehud Y. Shapiro: Communication with Directed Logic Variables. POPL 1991: 221-232

Thomas A. Henzinger, Zohar Manna, Amir Pnueli: Temporal Proof Methodologies for Real-time Systems. POPL 1991: 353-366

Thomas A. Henzinger, Zohar Manna, Amir Pnueli: Timed Transition Systems. REX Workshop 1991: 226-251

Oded Maler, Zohar Manna, Amir Pnueli: From Timed to Hybrid Systems. REX Workshop 1991: 447-484

Amir Pnueli, M. Shalev: What is in a Step: On the Semantics of Statecharts. TACS 1991: 244-264

David Harel, Hagi Lachover, Amnon Naamad, Amir Pnueli, Michal Politi, Rivi Sherman, Aharon Shtull-Trauring, Mark B. Trakhtenbrot: STATEMATE: A Working Environment for the Development of Complex Reactive Systems. IEEE Trans. Software Eng. 16(4): 403-414 (1990)

Oded Maler, Amir Pnueli: Tight Bounds on the Complexity of Cascaded Decomposition of Automata. FOCS 1990: 672-682

Amir Pnueli, Roni Rosner: Distributed Reactive Systems Are Hard to Synthesize. FOCS 1990: 746-757

Doron Peled, Amir Pnueli: Proving Partial Order Liveness Properties. ICALP 1990: 553-571

Eyal Harel, Orna Lichtenstein, Amir Pnueli: Explicit Clock Temporal Logic. LICS 1990: 402-413

Zohar Manna, Amir Pnueli: A Hierarchy of Temporal Properties. PODC 1990: 377-410

Oded Maler, Amir Pnueli: Learning omega-Regular Languages from Queries and Counter-Examples (A Preliminary Report). AII 1989: 161-170

Zohar Manna, Amir Pnueli: Completing the Temporal Picture. ICALP 1989: 534-558

Amir Pnueli, Roni Rosner: On the Synthesis of an Asynchronous Reactive Module. ICALP 1989: 652-671

Amir Pnueli, Roni Rosner: On the Synthesis of a Reactive Module. POPL 1989: 179-190

Behnam Banieqbal, Howard Barringer, Amir Pnueli (Eds.): Temporal Logic in Specification, Altrincham, UK, April 8-10, 1987, Proceedings. Lecture Notes in Computer Science 398, Springer 1989, isbn 3-540-51803-7

Dov Dori, Amir Pnueli: The grammar of dimensions in machine drawings. Computer Vision, Graphics, and Image Processing 42(1): 1-18 (1988)

Amir Pnueli, Roni Rosner: A Framework for the Synthesis of Reactive Modules. Concurrency 1988: 4-17

Amir Pnueli, Eyal Harel: Applications of Temporal Logic to the Specification of Real-time Systems. FTRTFT 1988: 84-98

David Harel, Hagi Lachover, Amnon Naamad, Amir Pnueli, Michal Politi, Rivi Sherman, Aharon Shtull-Trauring: STATEMATE; A Working Environment for the Development of Complex Reactive Systems. ICSE 1988: 396-406

Zohar Manna, Amir Pnueli: The anchored version of the temporal framework. REX Workshop 1988: 201-284

Yuan Shi, Noah S. Prywes, Boleslaw K. Szymanski, Amir Pnueli: Very High Level Concurrent Programming. IEEE Trans. Software Eng. 13(9): 1038-1046 (1987)

David Harel, Amir Pnueli, Jeanette P. Schmidt, Rivi Sherman: On the Formal Semantics of Statecharts (Extended Abstract). LICS 1987: 54-64

Zohar Manna, Amir Pnueli: A Hierarchy of Temporal Properties (Abstract). PODC 1987: 205

Zohar Manna, Amir Pnueli: Specification and Verification of Concurrent Programs By Forall-Automata. POPL 1987: 1-12

S. Kaplan, Amir Pnueli: Specification and Implementation of Concurrently Accessed Data Structures: An Abstract Data Type Approach. STACS 1987: 220-244

Zohar Manna, Amir Pnueli: Specification and Verification of Concurrent Programs by forall-Automata. Temporal Logic in Specification 1987: 124-164

Amir Pnueli, Lenore D. Zuck: Verification of Multiprocess Probabilistic Protocols. Distributed Computing 1(1): 53-72 (1986)

Amir Pnueli: Specification and Development of Reactive Systems (Invited Paper). IFIP Congress 1986: 845-858

Roni Rosner, Amir Pnueli: A Choppy Logic. LICS 1986: 306-313

Amir Pnueli, Lenore D. Zuck: Probabilistic Verification by Tableaux. LICS 1986: 322-331

Howard Barringer, Ruurd Kuiper, Amir Pnueli: A Really Abstract Concurrent Model and its Temporal Logic. POPL 1986: 173-183

Amir Pnueli: Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends. Current Trends in Concurrency 1986: 510-584

Amir Pnueli: Linear and Branching Structures in the Semantics and Logics of Reactive Systems. ICALP 1985: 15-32

Nissim Francez, Orna Grumberg, Shmuel Katz, Amir Pnueli: Proving Termination of Prolog Programs. Logic of Programs 1985: 89-105

Orna Lichtenstein, Amir Pnueli, Lenore D. Zuck: The Glory of the Past. Logic of Programs 1985: 196-218

Orna Lichtenstein, Amir Pnueli: Checking That Finite State Concurrent Programs Satisfy Their Linear Specification. POPL 1985: 97-107

Zohar Manna, Amir Pnueli: Adequate Proof Principles for Invariance and Liveness Properties of Concurrent Programs. Sci. Comput. Program. 4(3): 257-289 (1984)

Micha Sharir, Amir Pnueli, Sergiu Hart: Verification of Probabilistic Programs. SIAM J. Comput. 13(2): 292-314 (1984)

Rivi Sherman, Amir Pnueli, David Harel: Is the Interesting Part of Process Logic Uninteresting? A Translation from PL to PDL. SIAM J. Comput. 13(4): 825-839 (1984)

Nissim Francez, Daniel J. Lehmann, Amir Pnueli: A Linear-History Semantics for Languages for Distributed Programming. Theor. Comput. Sci. 32: 25-46 (1984)

Krzysztof R. Apt, Amir Pnueli, Jonathan Stavi: Fair Termination Revisited-With Delay. Theor. Comput. Sci. 33: 65-84 (1984)

Shimon Cohen, Daniel J. Lehmann, Amir Pnueli: Symmetric and Economical Solutions to the Mutual Exclusion Problem in a Distributed System. Theor. Comput. Sci. 34: 215-225 (1984)

Boleslaw K. Szymanski, Noah S. Prywes, Evan D. Lock, Amir Pnueli: On the scope of static checking in definitional languages. ACM Conference on Computer Science 1984: 197-207

Dorit Ron, Flavia Rosemberg, Amir Pnueli: A Hardware Implementation of the CSP Primitives and its Verification. ICALP 1984: 423-435

Amir Pnueli, Lenore D. Zuck: Verification of Multiprocess Probabilistic Protocols. PODC 1984: 12-27

Dennis Shasha, Amir Pnueli, W. Ewald: Temporal Verification of Carrier-Sense Local Area Network Protocols. POPL 1984: 54-65

Howard Barringer, Ruurd Kuiper, Amir Pnueli: Now You May Compose Temporal Logic Specifications. STOC 1984: 51-63

Mordechai Ben-Ari, Amir Pnueli, Zohar Manna: The Temporal Logic of Branching Time. Acta Inf. 20: 207-226 (1983)

David Harel, Amir Pnueli, Jonathan Stavi: Propositional Dynamic Logic of Nonregular Programs. J. Comput. Syst. Sci. 26(2): 222-243 (1983)

Sergiu Hart, Micha Sharir, Amir Pnueli: Termination of Probabilistic Concurrent Program. ACM Trans. Program. Lang. Syst. 5(3): 356-380 (1983)

Noah S. Prywes, Amir Pnueli: Compilation of Nonprocedural Specifications into Computer Programs. IEEE Trans. Software Eng. 9(3): 267-279 (1983)

Amir Pnueli: Solutions to Problem No.2. The Analysis of Concurrent Systems 1983: 365-383

Shimon Cohen, Daniel J. Lehmann, Amir Pnueli: Symmetric and Economical Solutions to the Mutual Exclusion Problem in a Distributed System (Extended Abstract). ICALP 1983: 128-136

Zohar Manna, Amir Pnueli: Proving Precedence Properties: The Temporal Way. ICALP 1983: 491-512

Tmima Koren, Amir Pnueli: There Exit Decidable Context Free Propositional Dynamic Logics. Logic of Programs 1983: 290-312

Zohar Manna, Amir Pnueli: How to Cook a Temporal Proof System for Your Pet Language. POPL 1983: 141-154

Amir Pnueli: On the Extremely Fair Treatment of Probabilistic Algorithms. STOC 1983: 278-290

Mordechai Ben-Ari, Joseph Y. Halpern, Amir Pnueli: Deterministic Propositional Dynamic Logic: Finite Models, Complexity, and Completeness. J. Comput. Syst. Sci. 25(3): 402-417 (1982)

Sergiu Hart, Micha Sharir, Amir Pnueli: Termination of Probabilistic Concurrent Programs. POPL 1982: 1-6

Rivi Sherman, Amir Pnueli, David Harel: Is the Interesting Part of Process Logic Uninteresting - A Translation from PL to PDL. POPL 1982: 347-360

Amir Pnueli, Giora Slutzki: Automatic Programming of Finite State Linear Programs. SIAM J. Comput. 10(3): 519-535 (1981)

Amir Pnueli: The Temporal Semantics of Concurrent Programs. Theor. Comput. Sci. 13: 45-60 (1981)

David Harel, Amir Pnueli, Jonathan Stavi: Propositional Dynamic Logic of Context-Free Programs. FOCS 1981: 310-321

Mordechai Ben-Ari, Joseph Y. Halpern, Amir Pnueli: Finite Models for Deterministic Propositional Dynamic Logic. ICALP 1981: 249-263

Daniel J. Lehmann, Amir Pnueli, Jonathan Stavi: Impartiality, Justice and Fairness: The Ethics of Concurrent Termination. ICALP 1981: 264-277

Amir Pnueli, R. Zarhi: Realizing an Equational Specification. ICALP 1981: 459-478

David Harel, Amir Pnueli, Jonathan Stavi: Further Results on Propositional Dynamic Logic of Nonregular Programs. Logic of Programs 1981: 124-136

Zohar Manna, Amir Pnueli: Verification of Concurrent Programs: Temporal Proof Principles. Logic of Programs 1981: 200-252

Mordechai Ben-Ari, Zohar Manna, Amir Pnueli: The Temporal Logic of Branching Time. POPL 1981: 164-176

Nissim Francez, Daniel J. Lehmann, Amir Pnueli: A Linear History Semantics for Distributed Languages (Extended Abstract). FOCS 1980: 143-151

Zohar Manna, Amir Pnueli: Synchronous Schemes and Their Decision Problems. POPL 1980: 62-67

Dov M. Gabbay, Amir Pnueli, Saharon Shelah, Jonathan Stavi: On the Temporal Basis of Fairness. POPL 1980: 163-173

Noah S. Prywes, Amir Pnueli, S. Shastry: Use of a Nonprocedural Specification Language and Associated Program Generator in Software Development. ACM Trans. Program. Lang. Syst. 1(2): 196-217 (1979)

Zohar Manna, Amir Pnueli: The Modal Logic of Programs. ICALP 1979: 385-409

Amir Pnueli: The Temporal Semantics of Concurrent Programs. Semantics of Concurrent Computation 1979: 1-20

Nissim Francez, Amir Pnueli: A Proof Method for Cyclic Programs. Acta Inf. 9: 133-157 (1978)

Nissim Francez, Boris Klebansky, Amir Pnueli: Backtracking in Recursive Computations. Acta Inf. 8: 125-144 (1977)

Tmima Olshansky, Amir Pnueli: A Direct Algorithm for Checking Equivalence of LL(k) Grammars. Theor. Comput. Sci. 4(3): 321-349 (1977)

Amir Pnueli: The Temporal Logic of Programs. FOCS 1977: 46-57

Amir Pnueli, Giora Slutzki: Simple Programs and Their Decision Problems. ICALP 1977: 380-390

David Harel, Amir Pnueli, Jonathan Stavi: A Complete Axiomatic System for Proving Deductions about Recursive Programs. STOC 1977: 249-260

Zohar Manna, Amir Pnueli: Axiomatic Approach to Total Correctness of Programs. Acta Inf. 3: 243-263 (1974)

Edward A. Ashcroft, Zohar Manna, Amir Pnueli: Decidable Properties of Monadic Functional Schemas. J. ACM 20(3): 489-499 (1973)

Shimon Even, Amir Pnueli, Abraham Lempel: Permutation Graphs and Transitive Graphs. J. ACM 19(3): 400-410 (1972)

F. Commoner, Anatol W. Holt, Shimon Even, Amir Pnueli: Marked Directed Graphs. J. Comput. Syst. Sci. 5(5): 511-523 (1971)

Zohar Manna, Amir Pnueli: Formalization of Properties of Functional Programs. J. ACM 17(3): 555-569 (1970)

Zohar Manna, Amir Pnueli: Formalization of Properties of Recursively Defined Functions. STOC 1969: 201-210