Amir Pnueli - RankMe

277 papers A* 74A 13B 28C 4Misc 4Journal 64Unranked 81

Year	Rank	Type	Title / Venue / Authors
2019	J	`jnl`	From Real-time Logic to Timed Automata. J. ACM Thomas Ferrère, Oded Maler, Dejan Nickovic, Amir Pnueli
2018	—	`ch.`	Temporal Logic and Fair Discrete Systems. Handbook of Model Checking Nir Piterman, Amir Pnueli
2012	B	`conf`	Effective Synthesis of Asynchronous Systems from GR(1) Specifications. VMCAI Uri Klein, Nir Piterman, Amir Pnueli
2012	J	`jnl`	Low dimensional hybrid systems - decidable, undecidable, don't know. Inf. Comput. Eugene Asarin, Venkatesh Mysore, Amir Pnueli, Gerardo Schneider
2012	J	`jnl`	Once and for all. J. Comput. Syst. Sci. Orna Kupferman, Amir Pnueli, Moshe Y. Vardi
2012	J	`jnl`	Synthesis of Reactive(1) designs. J. Comput. Syst. Sci. Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Yaniv Sa'ar
2012	J	`jnl`	Verification of multi-linked heaps. J. Comput. Syst. Sci. Ittai Balaban, Amir Pnueli, Yaniv Sa'ar, Lenore D. Zuck
2010	A*	`conf`	Jtlv: A Framework for Developing Verification Algorithms. CAV Amir Pnueli, Yaniv Sa'ar, Lenore D. Zuck
2010	—	`ed.`	Perspectives of Systems Informatics, 7th International Andrei Ershov Memorial Conference, PSI 2009, Novosibirsk, Russia, June 15-19, 2009. Revised Papers Ershov Memorial Conference Amir Pnueli, Irina B. Virbitskaite, Andrei Voronkov
2010	—	`conf`	Proving the Refuted: Symbolic Model Checkers as Proof Generators. Concurrency, Compositionality, and Correctness Ittai Balaban, Amir Pnueli, Lenore D. Zuck
2010	—	`conf`	Revisiting Synthesis of GR(1) Specifications. Haifa Verification Conference Uri Klein, Amir Pnueli
2010	—	`conf`	Temporal Verification of Reactive Systems: Response. Essays in Memory of Amir Pnueli Zohar Manna, Amir Pnueli
2010	—	`conf`	Towards Component Based Design of Hybrid Systems: Safety and Stability. Essays in Memory of Amir Pnueli Werner Damm, Henning Dierks, Jens Oehlerking, Amir Pnueli
2009	B	`conf`	Controller Synthesis from LSC Requirements. FASE Hillel Kugler, Cory Plock, Amir Pnueli
2009	C	`conf`	Synthesis of programs from temporal property specifications. MEMOCODE Amir Pnueli, Uri Klein
2008	J	`jnl`	A Sound and Complete Deductive System for CTL* Verification. Log. J. IGPL Dov M. Gabbay, Amir Pnueli
2008	B	`conf`	All You Need Is Compassion. VMCAI Amir Pnueli, Yaniv Sa'ar
2008	—	`conf`	Checking Temporal Properties of Discrete, Timed and Continuous Behaviors. Pillars of Computer Science Oded Maler, Dejan Nickovic, Amir Pnueli
2008	B	`conf`	CoVaC: Compiler Validation by Program Analysis of the Cross-Product. FM Anna Zaks, Amir Pnueli
2008	A*	`conf`	Discriminative Model Checking. CAV Peter Niebert, Doron A. Peled, Amir Pnueli
2008	A*	`conf`	Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses. CAV Ariel Cohen, Amir Pnueli, Lenore D. Zuck
2008	—	`conf`	On the Merits of Temporal Testers. 25 Years of Model Checking Amir Pnueli, Aleksandr Zaks
2008	—	`conf`	Program analysis for compiler validation. PASTE Anna Zaks, Amir Pnueli
2008	C	`conf`	Using Abstraction to Verify Arbitrary Temporal Properties. APSEC Amir Pnueli
2007	A	`conf`	"Don't Care" Modeling: A Logical Framework for Developing Predictive System Models. TACAS Hillel Kugler, Amir Pnueli, Michael J. Stern, E. Jane Albert Hubbard
2007	A	`conf`	Interactive presentation: Automatic hardware synthesis from specifications: a case study. DATE Roderick Bloem, Stefan J. Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Martin Weiglhofer
2007	J	`jnl`	Modular Ranking Abstraction. Int. J. Found. Comput. Sci. Ittai Balaban, Amir Pnueli, Lenore D. Zuck
2007	A*	`conf`	On Synthesizing Controllers from Bounded-Response Properties. CAV Oded Maler, Dejan Nickovic, Amir Pnueli
2007	B	`conf`	Shape Analysis of Single-Parent Heaps. VMCAI Ittai Balaban, Amir Pnueli, Lenore D. Zuck
2007	—	`conf`	Specify, Compile, Run: Hardware from PSL. COCV Roderick Bloem, Stefan J. Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Martin Weiglhofer
2007	—	`conf`	Synthesizing reactive systems from LSC requirements using the play-engine. OOPSLA Companion Hillel Kugler, Cory Plock, Amir Pnueli
2007	B	`conf`	Verifying Correctness of Transactional Memories. FMCAD Ariel Cohen, John W. O'Leary, Amir Pnueli, Mark R. Tuttle, Lenore D. Zuck
2006	A*	`conf`	Faster Solutions of Rabin and Streett Games. LICS Nir Piterman, Amir Pnueli
2006	—	`conf`	From MITL to Timed Automata. FORMATS Oded Maler, Dejan Nickovic, Amir Pnueli
2006	—	`conf`	Invisible Safety of Distributed Protocols. ICALP (2) Ittai Balaban, Amir Pnueli, Lenore D. Zuck
2006	C	`conf`	Liveness by Invisible Invariants. FORTE Yi Fang, Kenneth L. McMillan, Amir Pnueli, Lenore D. Zuck
2006	J	`jnl`	Liveness with invisible ranking. Int. J. Softw. Tools Technol. Transf. Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck
2006	J	`jnl`	Model Checking with Strong Fairness. Formal Methods Syst. Des. Yonit Kesten, Amir Pnueli, Li-on Raviv, Elad Shahar
2006	B	`conf`	PSL Model Checking and Run-Time Verification Via Testers. FM Amir Pnueli, Aleksandr Zaks
2006	B	`conf`	Ranking Abstraction of Recursive Programs. VMCAI Ittai Balaban, Ariel Cohen, Amir Pnueli
2006	B	`conf`	Synthesis of Reactive(1) Designs. VMCAI Nir Piterman, Amir Pnueli, Yaniv Sa'ar
2005	J	`jnl`	A compositional approach to CTL* verification. Theor. Comput. Sci. Yonit Kesten, Amir Pnueli
2005	J	`jnl`	A discrete-time UML semantics for concurrency and communication in safety-critical applications. Sci. Comput. Program. Werner Damm, Bernhard Josko, Amir Pnueli, Anjelika Votintseva
2005	B	`conf`	Abstraction for Liveness. VMCAI Amir Pnueli
2005	J	`jnl`	Bridging the gap between fair simulation and trace inclusion. Inf. Comput. Yonit Kesten, Nir Piterman, Amir Pnueli
2005	A*	`conf`	IIV: An Invisible Invariant Verifier. CAV Ittai Balaban, Yi Fang, Amir Pnueli, Lenore D. Zuck
2005	—	`conf`	Monitoring Interfaces for Faults. RV@CAV Amir Pnueli, Aleksandr Zaks, Lenore D. Zuck
2005	C	`conf`	Ranking Abstraction as Companion to Predicate Abstraction. FORTE Ittai Balaban, Amir Pnueli, Lenore D. Zuck
2005	B	`conf`	Ranking Abstraction as a Companion to Predicate Abstraction, . ATVA Amir Pnueli
2005	—	`conf`	Real Time Temporal Logic: Past, Present, Future. FORMATS Oded Maler, Dejan Nickovic, Amir Pnueli
2005	—	`conf`	Reduced Functional Consistency of Uninterpreted Functions. PDPAR@CAV Amir Pnueli, Ofer Strichman
2005	—	`conf`	Refining the Undecidability Frontier of Hybrid Automata. FSTTCS Venkatesh Mysore, Amir Pnueli
2005	A	`conf`	Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems. TACAS Amir Pnueli, Andreas Podelski, Andrey Rybalchenko
2005	B	`conf`	Shape Analysis by Predicate Abstraction. VMCAI Ittai Balaban, Amir Pnueli, Lenore D. Zuck
2005	—	`conf`	Synthesis Revisited: Generating Statechart Models from Scenario-Based Requirements. Formal Methods in Software and Systems Modeling David Harel, Hillel Kugler, Amir Pnueli
2005	A*	`conf`	TVOC: A Translation Validator for Optimizing Compilers. CAV Clark W. Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, Lenore D. Zuck
2005	A	`conf`	Temporal Logic for Scenario-Based Specifications. TACAS Hillel Kugler, David Harel, Amir Pnueli, Yuan Lu, Yves Bontemps
2005	J	`jnl`	Translation and Run-Time Validation of Loop Transformations. Formal Methods Syst. Des. Lenore D. Zuck, Amir Pnueli, Benjamin Goldberg, Clark W. Barrett, Yi Fang, Ying Hu
2005	—	`conf`	Validating More Loop Optimizations. COCV Ying Hu, Clark W. Barrett, Benjamin Goldberg, Amir Pnueli
2005	—	`conf`	Verification of Procedural Programs. We Will Show Them! (2) Amir Pnueli
2004	—	`conf`	Deductive Verification of UML Models in TLPVS. UML Tamarah Arons, Jozef Hooman, Hillel Kugler, Amir Pnueli, Mark van der Zwaag
2004	A	`conf`	Liveness with Incomprehensible Ranking. TACAS Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck
2004	B	`conf`	Liveness with Invisible Ranking. VMCAI Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck
2004	J	`jnl`	Model checking and abstraction to the aid of parameterized systems (a survey). Comput. Lang. Syst. Struct. Lenore D. Zuck, Amir Pnueli
2004	B	`conf`	On Recognizable Timed Languages. FoSSaCS Oded Maler, Amir Pnueli
2004	A*	`conf`	Range Allocation for Separation Logic. CAV Muralidhar Talupur, Nishant Sinha, Ofer Strichman, Amir Pnueli
2004	—	`conf`	Smart Play-Out Extended: Time and Forbidden Elements. QSIC David Harel, Hillel Kugler, Amir Pnueli
2004	B	`conf`	Validating the Translation of an Industrial Optimizing Compiler. ATVA I. Gordin, Raya Leviathan, Amir Pnueli
2003	A*	`conf`	Bridging the Gap between Fair Simulation and Trace Inclusion. CAV Yonit Kesten, Nir Piterman, Amir Pnueli
2003	J	`jnl`	Erratum ("The small model property: how small can it be?" Volume 178, Number 1 [2002], pages 279-293). Inf. Comput. Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel
2003	—	`conf`	Formal Modeling of C. elegans Development: A Scenario-Based Approach. CMSB Na'aman Kam, David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli, E. Jane Albert Hubbard, Michael J. Stern
2003	—	`ed.`	Hybrid Systems: Computation and Control, 6th International Workshop, HSCC 2003 Prague, Czech Republic, April 3-5, 2003, Proceedings Oded Maler, Amir Pnueli
2003	B	`conf`	Model-Checking and Abstraction to the Aid of Parameterized Systems. VMCAI Amir Pnueli, Lenore D. Zuck
2003	B	`conf`	Parameterized Verification by Probabilistic Abstraction. FoSSaCS Tamarah Arons, Amir Pnueli, Lenore D. Zuck
2003	—	`conf`	Smart play-out. OOPSLA Companion David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli
2003	—	`conf`	TLPVS: A PVS-Based LTL Verification System. Verification: Theory and Practice Amir Pnueli, Tamarah Arons
2003	—	`conf`	The ROBDD Size of Simple CNF Formulas. CHARME Michael Langberg, Amir Pnueli, Yoav Rodeh
2003	J	`jnl`	VOC: A Methodology for the Translation Validation of OptimizingCompilers. J. Univers. Comput. Sci. Lenore D. Zuck, Amir Pnueli, Benjamin Goldberg
2002	B	`conf`	A Deductive Proof System for CTL. CONCUR Amir Pnueli, Yonit Kesten
2002	—	`conf`	Applications of Formal Methods in Biology. FTRTFT Amir Pnueli
2002	B	`conf`	Automatic Verification of Probabilistic Free Choice. VMCAI Lenore D. Zuck, Amir Pnueli, Yonit Kesten
2002	J	`jnl`	Complete Proof System for QPTL. J. Log. Comput. Yonit Kesten, Amir Pnueli
2002	Misc	`conf`	Embedded Systems: Challenges in Specification and Verification. EMSOFT Amir Pnueli
2002	A*	`conf`	Liveness with (0, 1, infty)-Counter Abstraction. CAV Amir Pnueli, Jessie Xu, Lenore D. Zuck
2002	B	`conf`	Network Invariants in Action. CONCUR Yonit Kesten, Amir Pnueli, Elad Shahar, Lenore D. Zuck
2002	B	`conf`	Smart Play-out of Behavioral Requirements. FMCAD David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli
2002	J	`jnl`	The Small Model Property: How Small Can It Be? Inf. Comput. Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel
2002	J	`jnl`	TimeC: A Time Constraint Language for ILP Processor Compilation. Constraints An Int. J. Allen Leung, Krishna V. Palem, Amir Pnueli
2002	—	`conf`	Translation and Run-Time Validation of Optimized Code. RV@FLoC Lenore D. Zuck, Amir Pnueli, Yi Fang, Benjamin Goldberg, Ying Hu
2002	—	`conf`	Understanding UML: A Formal Semantics of Concurrency and Communication in Real-Time UML. FMCO Werner Damm, Bernhard Josko, Amir Pnueli, Anjelika Votintseva
2002	—	`conf`	VOC: A Translation Validator for Optimizing Compilers. COCV Lenore D. Zuck, Amir Pnueli, Yi Fang, Benjamin Goldberg
2002	Misc	`conf`	Validating software pipelining optimizations. CASES Raya Leviathan, Amir Pnueli
2001	A	`conf`	Automatic Deductive Verification with Invisible Invariants. TACAS Amir Pnueli, Sitvanit Ruah, Lenore D. Zuck
2001	—	`conf`	Beyond Regular Model Checking. FSTTCS Dana Fisman, Amir Pnueli
2001	—	`conf`	From Falsification to Verification. FSTTCS Doron A. Peled, Amir Pnueli, Lenore D. Zuck
2001	A*	`conf`	Parameterized Verification with Automatically Computed Inductive Assertions. CAV Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Jiazhao Xu, Lenore D. Zuck
2001	—	`conf`	Range Allocation for Equivalence Logic. FSTTCS Amir Pnueli, Yoav Rodeh, Ofer Strichman
2001	J	`jnl`	Scheduling time-constrained instructions on pipelined processors. ACM Trans. Program. Lang. Syst. Allen Leung, Krishna V. Palem, Amir Pnueli
2001	A*	`conf`	Sticks and stones: a coding scheme for parameterized verification. PODC Amir Pnueli
2001	J	`jnl`	Symbolic model checking with rich assertional languages. Theor. Comput. Sci. Yonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, Elad Shahar
2001	J	`jnl`	Verification by Augmented Abstraction: The Automata-Theoretic View. J. Comput. Syst. Sci. Yonit Kesten, Amir Pnueli, Moshe Y. Vardi
2000	A	`conf`	A Comparison of Two Verification Methods for Speculative Instruction Execution. TACAS Tamarah Arons, Amir Pnueli
2000	J	`jnl`	Control and Data Abstraction: The Cornerstones of Practical Formal Verification. Int. J. Softw. Tools Technol. Transf. Yonit Kesten, Amir Pnueli
2000	J	`jnl`	Effective synthesis of switching controllers for linear systems. Proc. IEEE Eugene Asarin, Olivier Bournez, Thao Dang, Oded Maler, Amir Pnueli
2000	—	`conf`	Formal Verification of the Ricart-Agrawala Algorithm. FSTTCS Ekaterina Sedletsky, Amir Pnueli, Mordechai Ben-Ari
2000	A*	`conf`	Keynote Address: Abstraction, Composition, Symmetry, and a Little Deduction: The Remedies to State Explosion. CAV Amir Pnueli
2000	A*	`conf`	Liveness and Acceleration in Parameterized Verification. CAV Amir Pnueli, Elad Shahar
2000	J	`jnl`	Propositional Temporal Logics: Decidability and Completeness. Log. J. IGPL Orna Lichtenstein, Amir Pnueli
2000	Misc	`conf`	Rigorous development of embedded systems. CASES Amir Pnueli
2000	J	`jnl`	Verification by Augmented Finitary Abstraction. Inf. Comput. Yonit Kesten, Amir Pnueli
2000	J	`jnl`	Verification of Clocked and Hybrid Systems. Acta Informatica Yonit Kesten, Zohar Manna, Amir Pnueli
1999	A	`conf`	A Framework for Scheduler Synthesis. RTSS Karine Altisen, Gregor Gößler, Amir Pnueli, Joseph Sifakis, Stavros Tripakis, Sergio Yovine
1999	—	`conf`	A Perfect Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software. World Congress on Formal Methods Yonit Kesten, Amit Klein, Amir Pnueli, Gil Raanan
1999	J	`jnl`	Decidable Integration Graphs. Inf. Comput. Yonit Kesten, Amir Pnueli, Joseph Sifakis, Sergio Yovine
1999	A*	`conf`	Deciding Equality Formulas by Small Domains Instantiations. CAV Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel
1999	—	`conf`	Orthogonal Polyhedra: Representation and Computation. HSCC Olivier Bournez, Oded Maler, Amir Pnueli
1999	J	`jnl`	Proving Refinement Using Transduction. Distributed Comput. Bengt Jonsson, Amir Pnueli, Camilla Rump
1999	—	`conf`	Translation Validation: From SIGNAL to C. Correct System Design Amir Pnueli, Ofer Strichman, Michael Siegel
1999	B	`conf`	Verifying Liveness by Augmented Abstraction. CSL Yonit Kesten, Amir Pnueli
1999	Misc	`conf`	Verifying Tomasulo's Algoithm by Refinement. VLSI Design Tamarah Arons, Amir Pnueli
1998	—	`conf`	A Fast Algorithm for Scheduling Time-Constrained Instructions on Processors with ILP. IEEE PACT Allen Leung, Krishna V. Palem, Amir Pnueli
1998	A*	`conf`	Algorithmic Verification of Linear Temporal Logic Specifications. ICALP Yonit Kesten, Amir Pnueli, Li-on Raviv
1998	—	`ed.`	Compositionality: The Significant Difference, International Symposium, COMPOS'97, Bad Malente, Germany, September 8-12, 1997. Revised Lectures COMPOS Willem P. de Roever, Hans Langmaack, Amir Pnueli
1998	A	`conf`	Deductive vs. Model-Theoretic Approaches to Formal Verification (Abstract of Invited Talk). CADE Amir Pnueli
1998	—	`conf`	Fair Synchronous Transition Systems and Their Liveness Proofs. FTRTFT Amir Pnueli, Natarajan Shankar, Eli Singerman
1998	B	`conf`	Herbrand Automata for Hardware Verification. CONCUR Werner Damm, Amir Pnueli, Sitvanit Ruah
1998	B	`conf`	Modularization and Abstraction: The Keys to Practical Formal Verification. MFCS Yonit Kesten, Amir Pnueli
1998	B	`conf`	On Discretization of Delays in Timed Automata and Digital Circuits. CONCUR Eugene Asarin, Oded Maler, Amir Pnueli
1998	J	`jnl`	The Code Validation Tool CVT: Automatic Verification of a Compilation Process. Int. J. Softw. Tools Technol. Transf. Amir Pnueli, Ofer Strichman, Michael Siegel
1998	A*	`conf`	Translation Validation for Synchronous Languages. ICALP Amir Pnueli, Ofer Strichman, Michael Siegel
1998	A	`conf`	Translation Validation. TACAS Amir Pnueli, Michael Siegel, Eli Singerman
1998	—	`conf`	Translation Validation: From DC+ to C*. FM-Trends Amir Pnueli, Ofer Strichman, Michael Siegel
1998	B	`conf`	Verification of Data-Insensitive CIrcuits: An In-Order-Retirement Case Study. FMCAD Amir Pnueli, Tamarah Arons
1997	—	`conf`	A Compositional Real-Time Semantics of STATEMATE Designs. COMPOS Werner Damm, Bernhard Josko, Hardi Hungar, Amir Pnueli
1997	—	`conf`	Data-Structures for the Verification of Timed Automata. HART Eugene Asarin, Marius Bozga, Alain Kerbrat, Oded Maler, Amir Pnueli, Anne Rasse
1997	A*	`conf`	Some Progress in the Symbolic Verification of Timed Automata. CAV Marius Bozga, Oded Maler, Amir Pnueli, Sergio Yovine
1997	A*	`conf`	Symbolic Model Checking with Rich ssertional Languages. CAV Yonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, Elad Shahar
1997	A*	`conf`	Two Decades of Temporal Logic: Achievements and Challenges (Abstract). FOCS Amir Pnueli
1997	A*	`conf`	Verification Engineering: A Future Profession (A. M. Turing Award Lecture). PODC Amir Pnueli
1997	—	`conf`	Verifying Liveness Properties of Reactive Systems (Tutorial Abstract). HART Amir Pnueli
1997	—	`conf`	Verifying out-of-order executions. CHARME Werner Damm, Amir Pnueli
1996	A*	`conf`	A Platform for Combining Deductive with Algorithmic Verification. CAV Amir Pnueli, Elad Shahar
1996	—	`conf`	Using Ghost Variables to Prove Refinement. AMAST Monica Marcus, Amir Pnueli
1996	—	`conf`	Verification of Clocked and Hybrid Systems. European Educational Forum: School on Embedded Systems Yonit Kesten, Zohar Manna, Amir Pnueli
1995	A*	`conf`	A Complete Proof Systems for QPTL LICS Yonit Kesten, Amir Pnueli
1995	J	`jnl`	On the Learnability of Infinitary Regular Sets Inf. Comput. Oded Maler, Amir Pnueli
1995	A	`conf`	On the Synthesis of Discrete Controllers for Timed Systems (An Extended Abstract). STACS Oded Maler, Amir Pnueli, Joseph Sifakis
1995	A*	`conf`	Once and For All LICS Orna Kupferman, Amir Pnueli
1995	J	`jnl`	Reachability Analysis of Dynamical Systems Having Piecewise-Constant Derivatives. Theor. Comput. Sci. Eugene Asarin, Oded Maler, Amir Pnueli
1995	—	`book`	Temporal verification of reactive systems - safety. Zohar Manna, Amir Pnueli
1995	—	`conf`	Timing analysis of asynchronous circuits using timed automata. CHARME Oded Maler, Amir Pnueli
1995	—	`conf`	Verifying Clocked Transition Systems. Hybrid Systems Yonit Kesten, Zohar Manna, Amir Pnueli
1994	A*	`conf`	Compositional Verification of Real-Time Systems LICS Edward Y. Chang, Zohar Manna, Amir Pnueli
1994	—	`conf`	Development of Hybrid Systems. FTRTFT Amir Pnueli
1994	—	`conf`	Prooving Safety Properties of Hybrid Systems. FTRTFT Arjun Kapur, Thomas A. Henzinger, Zohar Manna, Amir Pnueli
1994	J	`jnl`	Proving Partial Order Properties. Theor. Comput. Sci. Doron A. Peled, Amir Pnueli
1994	—	`conf`	Symbolic Controller Synthesis for Discrete and Timed Systems. Hybrid Systems Eugene Asarin, Oded Maler, Amir Pnueli
1994	J	`jnl`	Temporal Proof Methodologies for Timed Transition Systems Inf. Comput. Thomas A. Henzinger, Zohar Manna, Amir Pnueli
1994	—	`conf`	Temporal Verification Diagrams. TACS Zohar Manna, Amir Pnueli
1993	A*	`conf`	A Decision Algorithm for Full Propositional Temporal Logic. CAV Yonit Kesten, Zohar Manna, Hugh McGuire, Amir Pnueli
1993	A*	`conf`	In and Out of Temporal Logic LICS Amir Pnueli, Lenore D. Zuck
1993	J	`jnl`	Models for Reactivity. Acta Informatica Zohar Manna, Amir Pnueli
1993	J	`jnl`	Probabilistic Verification Inf. Comput. Amir Pnueli, Lenore D. Zuck
1993	A*	`conf`	Reachability Analysis of Planar Multi-limear Systems. CAV Oded Maler, Amir Pnueli
1993	—	`conf`	Temporal Verification of Simulation and Refinement. REX School/Symposium Yonit Kesten, Zohar Manna, Amir Pnueli
1993	—	`ch.`	Verification of parameterized programs. Specification and validation methods Zohar Manna, Amir Pnueli
1992	—	`conf`	A Temporal Proof Methodology for Reactive Systems. NATO ASI PDC Zohar Manna, Amir Pnueli
1992	A*	`conf`	Characterization of Temporal Property Classes. ICALP Edward Y. Chang, Zohar Manna, Amir Pnueli
1992	B	`conf`	How Vital is Liveness? Verifying Timing Properties of Reactive and Hybrid Systems (Extended Abstract). CONCUR Amir Pnueli
1992	—	`conf`	Integration Graphs: A Class of Decidable Hybrid Systems. Hybrid Systems Yonit Kesten, Amir Pnueli, Joseph Sifakis, Sergio Yovine
1992	—	`conf`	System Specification and Refinement in Temporal Logic. FSTTCS Amir Pnueli
1992	—	`book`	The temporal logic of reactive and concurrent systems - specification. Zohar Manna, Amir Pnueli
1992	—	`conf`	Time for Concurrency. 25th Anniversary of INRIA Zohar Manna, Amir Pnueli
1992	—	`conf`	Timed and Hybrid Statecharts and Their Textual Representation. FTRTFT Yonit Kesten, Amir Pnueli
1992	—	`conf`	Towards Refining Temporal Specifications into Hybrid Systems. Hybrid Systems Thomas A. Henzinger, Zohar Manna, Amir Pnueli
1992	—	`conf`	Verifying Hybrid Systems. Hybrid Systems Zohar Manna, Amir Pnueli
1992	A*	`conf`	What Good Are Digital Clocks? ICALP Thomas A. Henzinger, Zohar Manna, Amir Pnueli
1991	A*	`conf`	Communication with Directed Logic Variables. POPL Alon Kleinman, Yael Moscowitz, Amir Pnueli, Ehud Shapiro
1991	J	`jnl`	Completing the Temporal Picture. Theor. Comput. Sci. Zohar Manna, Amir Pnueli
1991	—	`conf`	From Timed to Hybrid Systems. REX Workshop Oded Maler, Zohar Manna, Amir Pnueli
1991	B	`conf`	On the Faithfulness of Formal Models. MFCS Zohar Manna, Amir Pnueli
1991	A*	`conf`	On the Learnability of Infinitary Regular Sets. COLT Oded Maler, Amir Pnueli
1991	A*	`conf`	Specifying and Proving Serializability in Temporal Logic LICS Doron A. Peled, Shmuel Katz, Amir Pnueli
1991	A*	`conf`	Temporal Proof Methodologies for Real-time Systems. POPL Thomas A. Henzinger, Zohar Manna, Amir Pnueli
1991	—	`conf`	Timed Transition Systems. REX Workshop Thomas A. Henzinger, Zohar Manna, Amir Pnueli
1991	—	`conf`	What is in a Step: On the Semantics of Statecharts. TACS Amir Pnueli, M. Shalev
1990	A*	`conf`	A Hierarchy of Temporal Properties. PODC Zohar Manna, Amir Pnueli
1990	—	`conf`	A temporal proof methodology for reactive systems. Jerusalem Conference on Information Technology Zohar Manna, Amir Pnueli
1990	—	`conf`	An interleaving model for real-time. Jerusalem Conference on Information Technology Thomas A. Henzinger, Zohar Manna, Amir Pnueli
1990	A*	`conf`	Distributed Reactive Systems Are Hard to Synthesize FOCS Amir Pnueli, Roni Rosner
1990	A*	`conf`	Explicit Clock Temporal Logic LICS Eyal Harel, Orna Lichtenstein, Amir Pnueli
1990	A*	`conf`	Proving Partial Order Liveness Properties. ICALP Doron A. Peled, Amir Pnueli
1990	J	`jnl`	STATEMATE: A Working Environment for the Development of Complex Reactive Systems. IEEE Trans. Software Eng. David Harel, Hagi Lachover, Amnon Naamad, Amir Pnueli, Michal Politi, Rivi Sherman, Aharon Shtull-Trauring, Mark B. Trakhtenbrot
1990	A*	`conf`	Tight Bounds on the Complexity of Cascaded Decomposition of Automata FOCS Oded Maler, Amir Pnueli
1989	A*	`conf`	Completing the Temporal Picture. ICALP Zohar Manna, Amir Pnueli
1989	—	`conf`	Learning omega-Regular Languages from Queries and Counter-Examples (A Preliminary Report). AII Oded Maler, Amir Pnueli
1989	A*	`conf`	On the Synthesis of a Reactive Module. POPL Amir Pnueli, Roni Rosner
1989	A*	`conf`	On the Synthesis of an Asynchronous Reactive Module. ICALP Amir Pnueli, Roni Rosner
1989	—	`conf`	Rooting UNITY. IWSSD Rob Gerth, Amir Pnueli
1989	A	`conf`	Specification and verification of VLSI systems. ICCAD Asher Wilk, Amir Pnueli
1989	—	`ed.`	Temporal Logic in Specification, Altrincham, UK, April 8-10, 1987, Proceedings Temporal Logic in Specification Behnam Banieqbal, Howard Barringer, Amir Pnueli
1988	—	`conf`	A Framework for the Synthesis of Reactive Modules. Concurrency Amir Pnueli, Roni Rosner
1988	—	`conf`	Applications of Temporal Logic to the Specification of Real-time Systems. FTRTFT Amir Pnueli, Eyal Harel
1988	A*	`conf`	STATEMATE; A Working Environment for the Development of Complex Reactive Systems. ICSE David Harel, Hagi Lachover, Amnon Naamad, Amir Pnueli, Michal Politi, Rivi Sherman, Aharon Shtull-Trauring
1988	—	`conf`	The anchored version of the temporal framework. REX Workshop Zohar Manna, Amir Pnueli
1988	J	`jnl`	The grammar of dimensions in machine drawings. Comput. Vis. Graph. Image Process. Dov Dori, Amir Pnueli
1987	A*	`conf`	A Hierarchy of Temporal Properties (Abstract). PODC Zohar Manna, Amir Pnueli
1987	A*	`conf`	On the Formal Semantics of Statecharts (Extended Abstract) LICS David Harel, Amir Pnueli, Jeanette P. Schmidt, Rivi Sherman
1987	A	`conf`	Specification and Implementation of Concurrently Accessed Data Structures: An Abstract Data Type Approach. STACS S. Kaplan, Amir Pnueli
1987	A*	`conf`	Specification and Verification of Concurrent Programs By Forall-Automata. POPL Zohar Manna, Amir Pnueli
1987	—	`conf`	Specification and Verification of Concurrent Programs by forall-Automata. Temporal Logic in Specification Zohar Manna, Amir Pnueli
1987	J	`jnl`	Very High Level Concurrent Programming. IEEE Trans. Software Eng. Yuan Shi, Noah S. Prywes, Boleslaw K. Szymanski, Amir Pnueli
1986	A*	`conf`	A Choppy Logic LICS Roni Rosner, Amir Pnueli
1986	A*	`conf`	A Really Abstract Concurrent Model and its Temporal Logic. POPL Howard Barringer, Ruurd Kuiper, Amir Pnueli
1986	—	`ch.`	Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends. Current Trends in Concurrency Amir Pnueli
1986	A*	`conf`	Probabilistic Verification by Tableaux LICS Amir Pnueli, Lenore D. Zuck
1986	—	`conf`	Specification and Development of Reactive Systems (Invited Paper). IFIP Congress Amir Pnueli
1986	J	`jnl`	Verification of Multiprocess Probabilistic Protocols. Distributed Comput. Amir Pnueli, Lenore D. Zuck
1985	A*	`conf`	Checking That Finite State Concurrent Programs Satisfy Their Linear Specification. POPL Orna Lichtenstein, Amir Pnueli
1985	A*	`conf`	Linear and Branching Structures in the Semantics and Logics of Reactive Systems. ICALP Amir Pnueli
1985	—	`conf`	Proving Termination of Prolog Programs. Logic of Programs Nissim Francez, Orna Grumberg, Shmuel Katz, Amir Pnueli
1985	—	`conf`	The Glory of the Past. Logic of Programs Orna Lichtenstein, Amir Pnueli, Lenore D. Zuck
1984	A*	`conf`	A Hardware Implementation of the CSP Primitives and its Verification. ICALP Dorit Ron, Flavia Rosemberg, Amir Pnueli
1984	J	`jnl`	A Linear-History Semantics for Languages for Distributed Programming. Theor. Comput. Sci. Nissim Francez, Daniel Lehmann, Amir Pnueli
1984	J	`jnl`	Adequate Proof Principles for Invariance and Liveness Properties of Concurrent Programs. Sci. Comput. Program. Zohar Manna, Amir Pnueli
1984	J	`jnl`	Automatic program generation in distributed cooperative computation. IEEE Trans. Syst. Man Cybern. Noah S. Prywes, Amir Pnueli
1984	J	`jnl`	Fair Termination Revisited-With Delay. Theor. Comput. Sci. Krzysztof R. Apt, Amir Pnueli, Jonathan Stavi
1984	—	`conf`	In Transition From Global to Modular Temporal Reasoning about Programs. Logics and Models of Concurrent Systems Amir Pnueli
1984	J	`jnl`	Is the Interesting Part of Process Logic Uninteresting? A Translation from PL to PDL. SIAM J. Comput. Rivi Sherman, Amir Pnueli, David Harel
1984	A*	`conf`	Now You May Compose Temporal Logic Specifications STOC Howard Barringer, Ruurd Kuiper, Amir Pnueli
1984	—	`conf`	On the Development of Reactive Systems. Logics and Models of Concurrent Systems David Harel, Amir Pnueli
1984	—	`conf`	On the scope of static checking in definitional languages. ACM Annual Conference Boleslaw K. Szymanski, Noah S. Prywes, Evan D. Lock, Amir Pnueli
1984	J	`jnl`	Symmetric and Economical Solutions to the Mutual Exclusion Problem in a Distributed System. Theor. Comput. Sci. Shimon Cohen, Daniel Lehmann, Amir Pnueli
1984	A*	`conf`	Temporal Verification of Carrier-Sense Local Area Network Protocols. POPL Dennis E. Shasha, Amir Pnueli, W. Ewald
1984	A*	`conf`	Verification of Multiprocess Probabilistic Protocols. PODC Amir Pnueli, Lenore D. Zuck
1984	J	`jnl`	Verification of Probabilistic Programs. SIAM J. Comput. Micha Sharir, Amir Pnueli, Sergiu Hart
1983	J	`jnl`	Compilation of Nonprocedural Specifications into Computer Programs. IEEE Trans. Software Eng. Noah S. Prywes, Amir Pnueli
1983	A*	`conf`	How to Cook a Temporal Proof System for Your Pet Language. POPL Zohar Manna, Amir Pnueli
1983	A*	`conf`	On the Extremely Fair Treatment of Probabilistic Algorithms STOC Amir Pnueli
1983	J	`jnl`	Propositional Dynamic Logic of Nonregular Programs. J. Comput. Syst. Sci. David Harel, Amir Pnueli, Jonathan Stavi
1983	A*	`conf`	Proving Precedence Properties: The Temporal Way. ICALP Zohar Manna, Amir Pnueli
1983	—	`conf`	Solutions to Problem No.2. The Analysis of Concurrent Systems Amir Pnueli
1983	A*	`conf`	Symmetric and Economical Solutions to the Mutual Exclusion Problem in a Distributed System (Extended Abstract). ICALP Shimon Cohen, Daniel Lehmann, Amir Pnueli
1983	J	`jnl`	Termination of Probabilistic Concurrent Program. ACM Trans. Program. Lang. Syst. Sergiu Hart, Micha Sharir, Amir Pnueli
1983	J	`jnl`	The Temporal Logic of Branching Time. Acta Informatica Mordechai Ben-Ari, Amir Pnueli, Zohar Manna
1983	—	`conf`	There Exit Decidable Context Free Propositional Dynamic Logics. Logic of Programs Tmima Koren, Amir Pnueli
1982	J	`jnl`	Deterministic Propositional Dynamic Logic: Finite Models, Complexity, and Completeness. J. Comput. Syst. Sci. Mordechai Ben-Ari, Joseph Y. Halpern, Amir Pnueli
1982	A*	`conf`	Is the Interesting Part of Process Logic Uninteresting - A Translation from PL to PDL. POPL Rivi Sherman, Amir Pnueli, David Harel
1982	—	`conf`	Rendezvous with ADA: a proof theoretical view. AdaTEC Conference on Ada Amir Pnueli, Willem P. de Roever
1982	A*	`conf`	Termination of Probabilistic Concurrent Programs. POPL Sergiu Hart, Micha Sharir, Amir Pnueli
1981	J	`jnl`	Automatic Programming of Finite State Linear Programs. SIAM J. Comput. Amir Pnueli, Giora Slutzki
1981	A*	`conf`	Finite Models for Deterministic Propositional Dynamic Logic. ICALP Mordechai Ben-Ari, Joseph Y. Halpern, Amir Pnueli
1981	—	`conf`	Further Results on Propositional Dynamic Logic of Nonregular Programs. Logic of Programs David Harel, Amir Pnueli, Jonathan Stavi
1981	A*	`conf`	Impartiality, Justice and Fairness: The Ethics of Concurrent Termination. ICALP Daniel Lehmann, Amir Pnueli, Jonathan Stavi
1981	A*	`conf`	Propositional Dynamic Logic of Context-Free Programs FOCS David Harel, Amir Pnueli, Jonathan Stavi
1981	A*	`conf`	Realizing an Equational Specification. ICALP Amir Pnueli, R. Zarhi
1981	A*	`conf`	The Temporal Logic of Branching Time. POPL Mordechai Ben-Ari, Zohar Manna, Amir Pnueli
1981	J	`jnl`	The Temporal Semantics of Concurrent Programs. Theor. Comput. Sci. Amir Pnueli
1981	—	`conf`	Verification of Concurrent Programs: Temporal Proof Principles. Logic of Programs Zohar Manna, Amir Pnueli
1980	A*	`conf`	A Linear History Semantics for Distributed Languages (Extended Abstract) FOCS Nissim Francez, Daniel Lehmann, Amir Pnueli
1980	A*	`conf`	On the Temporal Analysis of Fairness. POPL Dov M. Gabbay, Amir Pnueli, Saharon Shelah, Jonathan Stavi
1980	A*	`conf`	Synchronous Schemes and Their Decision Problems. POPL Zohar Manna, Amir Pnueli
1979	A*	`conf`	The Modal Logic of Programs. ICALP Zohar Manna, Amir Pnueli
1979	—	`conf`	The Temporal Semantics of Concurrent Programs. Semantics of Concurrent Computation Amir Pnueli
1979	J	`jnl`	Use of a Nonprocedural Specification Language and Associated Program Generator in Software Development. ACM Trans. Program. Lang. Syst. Noah S. Prywes, Amir Pnueli, S. Shastry
1978	J	`jnl`	A Proof Method for Cyclic Programs. Acta Informatica Nissim Francez, Amir Pnueli
1977	A*	`conf`	A Complete Axiomatic System for Proving Deductions about Recursive Programs STOC David Harel, Amir Pnueli, Jonathan Stavi
1977	J	`jnl`	A Direct Algorithm for Checking Equivalence of LL Theor. Comput. Sci. Tmima Olshansky, Amir Pnueli
1977	J	`jnl`	Backtracking in Recursive Computations. Acta Informatica Nissim Francez, Boris Klebansky, Amir Pnueli
1977	A*	`conf`	Simple Programs and Their Decision Problems. ICALP Amir Pnueli, Giora Slutzki
1977	A*	`conf`	The Temporal Logic of Programs FOCS Amir Pnueli
1974	J	`jnl`	Axiomatic Approach to Total Correctness of Programs. Acta Informatica Zohar Manna, Amir Pnueli
1973	J	`jnl`	Decidable Properties of Monadic Functional Schemas. J. ACM Edward A. Ashcroft, Zohar Manna, Amir Pnueli
1972	J	`jnl`	Permutation Graphs and Transitive Graphs. J. ACM Shimon Even, Amir Pnueli, Abraham Lempel
1971	J	`jnl`	Marked Directed Graphs. J. Comput. Syst. Sci. Frederic G. Commoner, Anatol W. Holt, Shimon Even, Amir Pnueli
1970	J	`jnl`	Formalization of Properties of Functional Programs. J. ACM Zohar Manna, Amir Pnueli
1969	A*	`conf`	Formalization of Properties of Recursively Defined Functions STOC Zohar Manna, Amir Pnueli