Amir Pnueli

According to our database, Amir Pnueli authored at least 262 papers between 1969 and 2019.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of two.

2019

From Real-time Logic to Timed Automata.

Thomas Ferrère, Oded Maler, Dejan Nickovic, Amir Pnueli

J. ACM, 2019

2018

Temporal Logic and Fair Discrete Systems.

Nir Piterman, Amir Pnueli

Proceedings of the Handbook of Model Checking., 2018

2012

Once and for all.

Orna Kupferman, Amir Pnueli, Moshe Y. Vardi

J. Comput. Syst. Sci., 2012

Synthesis of Reactive(1) designs.

Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Yaniv Sa'ar

J. Comput. Syst. Sci., 2012

Verification of multi-linked heaps.

Ittai Balaban, Amir Pnueli, Yaniv Sa'ar, Lenore D. Zuck

J. Comput. Syst. Sci., 2012

Low dimensional hybrid systems - decidable, undecidable, don't know.

Eugene Asarin, Venkatesh Mysore, Amir Pnueli, Gerardo Schneider

Inf. Comput., 2012

Effective Synthesis of Asynchronous Systems from GR(1) Specifications.

Uri Klein, Nir Piterman, Amir Pnueli

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012

2010

Revisiting Synthesis of GR(1) Specifications.

Uri Klein, Amir Pnueli

Proceedings of the Hardware and Software: Verification and Testing, 2010

Jtlv: A Framework for Developing Verification Algorithms.

Amir Pnueli, Yaniv Sa'ar, Lenore D. Zuck

Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

Temporal Verification of Reactive Systems: Response.

Zohar Manna, Amir Pnueli

Proceedings of the Time for Verification, 2010

Towards Component Based Design of Hybrid Systems: Safety and Stability.

Werner Damm, Henning Dierks, Jens Oehlerking, Amir Pnueli

Proceedings of the Time for Verification, 2010

Proving the Refuted: Symbolic Model Checkers as Proof Generators.

Ittai Balaban, Amir Pnueli, Lenore D. Zuck

Proceedings of the Concurrency, 2010

2009

Synthesis of programs from temporal property specifications.

Amir Pnueli, Uri Klein

Proceedings of the 7th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2009), 2009

Controller Synthesis from LSC Requirements.

Hillel Kugler, Cory Plock, Amir Pnueli

Proceedings of the Fundamental Approaches to Software Engineering, 2009

2008

A Sound and Complete Deductive System for CTL* Verification.

Dov M. Gabbay, Amir Pnueli

Log. J. IGPL, 2008

All You Need Is Compassion.

Amir Pnueli, Yaniv Sa'ar

Proceedings of the Verification, 2008

On the Merits of Temporal Testers.

Amir Pnueli, Aleksandr Zaks

Proceedings of the 25 Years of Model Checking - History, Achievements, Perspectives, 2008

Program analysis for compiler validation.

Anna Zaks, Amir Pnueli

Proceedings of the 8th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, 2008

CoVaC: Compiler Validation by Program Analysis of the Cross-Product.

Anna Zaks, Amir Pnueli

Proceedings of the FM 2008: Formal Methods, 2008

Discriminative Model Checking.

Peter Niebert, Doron A. Peled, Amir Pnueli

Proceedings of the Computer Aided Verification, 20th International Conference, 2008

Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses.

Ariel Cohen, Amir Pnueli, Lenore D. Zuck

Proceedings of the Computer Aided Verification, 20th International Conference, 2008

Checking Temporal Properties of Discrete, Timed and Continuous Behaviors.

Oded Maler, Dejan Nickovic, Amir Pnueli

Proceedings of the Pillars of Computer Science, 2008

Using Abstraction to Verify Arbitrary Temporal Properties.

Amir Pnueli

Proceedings of the 15th Asia-Pacific Software Engineering Conference (APSEC 2008), 2008

2007

Modular Ranking Abstraction.

Ittai Balaban, Amir Pnueli, Lenore D. Zuck

Int. J. Found. Comput. Sci., 2007

Specify, Compile, Run: Hardware from PSL.

Roderick Bloem, Stefan J. Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Martin Weiglhofer

Proceedings of the Workshop on Compiler Optimization meets Compiler Verification, 2007

Shape Analysis of Single-Parent Heaps.

Ittai Balaban, Amir Pnueli, Lenore D. Zuck

Proceedings of the Verification, 2007

"Don't Care" Modeling: A Logical Framework for Developing Predictive System Models.

Hillel Kugler, Amir Pnueli, Michael J. Stern, E. Jane Albert Hubbard

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Synthesizing reactive systems from LSC requirements using the play-engine.

Hillel Kugler, Cory Plock, Amir Pnueli

Proceedings of the Companion to the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2007

Verifying Correctness of Transactional Memories.

Ariel Cohen, John W. O'Leary, Amir Pnueli, Mark R. Tuttle, Lenore D. Zuck

Proceedings of the Formal Methods in Computer-Aided Design, 7th International Conference, 2007

Interactive presentation: Automatic hardware synthesis from specifications: a case study.

Roderick Bloem, Stefan J. Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Martin Weiglhofer

Proceedings of the 2007 Design, Automation and Test in Europe Conference and Exposition, 2007

On Synthesizing Controllers from Bounded-Response Properties.

Oded Maler, Dejan Nickovic, Amir Pnueli

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006

Liveness with invisible ranking.

Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck

Int. J. Softw. Tools Technol. Transf., 2006

Model Checking with Strong Fairness.

Yonit Kesten, Amir Pnueli, Li-on Raviv, Elad Shahar

Formal Methods Syst. Des., 2006

Synthesis of Reactive(1) Designs.

Nir Piterman, Amir Pnueli, Yaniv Sa'ar

Proceedings of the Verification, 2006

Ranking Abstraction of Recursive Programs.

Ittai Balaban, Ariel Cohen, Amir Pnueli

Proceedings of the Verification, 2006

Faster Solutions of Rabin and Streett Games.

Nir Piterman, Amir Pnueli

Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 2006

Invisible Safety of Distributed Protocols.

Ittai Balaban, Amir Pnueli, Lenore D. Zuck

Proceedings of the Automata, Languages and Programming, 33rd International Colloquium, 2006

Liveness by Invisible Invariants.

Yi Fang, Kenneth L. McMillan, Amir Pnueli, Lenore D. Zuck

Proceedings of the Formal Techniques for Networked and Distributed Systems, 2006

From MITL to Timed Automata.

Oded Maler, Dejan Nickovic, Amir Pnueli

Proceedings of the Formal Modeling and Analysis of Timed Systems, 2006

PSL Model Checking and Run-Time Verification Via Testers.

Amir Pnueli, Aleksandr Zaks

Proceedings of the FM 2006: Formal Methods, 2006

2005

A compositional approach to CTL* verification.

Yonit Kesten, Amir Pnueli

Theor. Comput. Sci., 2005

A discrete-time UML semantics for concurrency and communication in safety-critical applications.

Werner Damm, Bernhard Josko, Amir Pnueli, Anjelika Votintseva

Sci. Comput. Program., 2005

Bridging the gap between fair simulation and trace inclusion.

Yonit Kesten, Nir Piterman, Amir Pnueli

Inf. Comput., 2005

Translation and Run-Time Validation of Loop Transformations.

Lenore D. Zuck, Amir Pnueli, Benjamin Goldberg, Clark W. Barrett, Yi Fang, Ying Hu

Formal Methods Syst. Des., 2005

Monitoring Interfaces for Faults.

Amir Pnueli, Aleksandr Zaks, Lenore D. Zuck

Proceedings of the Fifth Workshop on Runtime Verification, 2005

Reduced Functional Consistency of Uninterpreted Functions.

Amir Pnueli, Ofer Strichman

Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning, 2005

Validating More Loop Optimizations.

Ying Hu, Clark W. Barrett, Benjamin Goldberg, Amir Pnueli

Proceedings of the Fourth International Workshop on Compiler Optimization meets Compiler Verification, 2005

Abstraction for Liveness.

Amir Pnueli

Proceedings of the Verification, 2005

Shape Analysis by Predicate Abstraction.

Ittai Balaban, Amir Pnueli, Lenore D. Zuck

Proceedings of the Verification, 2005

Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems.

Amir Pnueli, Andreas Podelski, Andrey Rybalchenko

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Temporal Logic for Scenario-Based Specifications.

Hillel Kugler, David Harel, Amir Pnueli, Yuan Lu, Yves Bontemps

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Refining the Undecidability Frontier of Hybrid Automata.

Venkatesh Mysore, Amir Pnueli

Proceedings of the FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 2005

Ranking Abstraction as Companion to Predicate Abstraction.

Ittai Balaban, Amir Pnueli, Lenore D. Zuck

Proceedings of the Formal Techniques for Networked and Distributed Systems, 2005

Real Time Temporal Logic: Past, Present, Future.

Oded Maler, Dejan Nickovic, Amir Pnueli

Proceedings of the Formal Modeling and Analysis of Timed Systems, 2005

TVOC: A Translation Validator for Optimizing Compilers.

Clark W. Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, Lenore D. Zuck

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

IIV: An Invisible Invariant Verifier.

Ittai Balaban, Yi Fang, Amir Pnueli, Lenore D. Zuck

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

Verification of Procedural Programs.

Amir Pnueli

Proceedings of the We Will Show Them! Essays in Honour of Dov Gabbay, Volume Two, 2005

Synthesis Revisited: Generating Statechart Models from Scenario-Based Requirements.

David Harel, Hillel Kugler, Amir Pnueli

Proceedings of the Formal Methods in Software and Systems Modeling, 2005

Ranking Abstraction as a Companion to Predicate Abstraction, .

Amir Pnueli

Proceedings of the Automated Technology for Verification and Analysis, 2005

2004

Model checking and abstraction to the aid of parameterized systems (a survey).

Lenore D. Zuck, Amir Pnueli

Comput. Lang. Syst. Struct., 2004

Deductive Verification of UML Models in TLPVS.

Tamarah Arons, Jozef Hooman, Hillel Kugler, Amir Pnueli, Mark van der Zwaag

Proceedings of the «UML» 2004, 2004

Liveness with Incomprehensible Ranking.

Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

Smart Play-Out Extended: Time and Forbidden Elements.

David Harel, Hillel Kugler, Amir Pnueli

Proceedings of the 4th International Conference on Quality Software (QSIC 2004), 2004

On Recognizable Timed Languages.

Oded Maler, Amir Pnueli

Proceedings of the Foundations of Software Science and Computation Structures, 2004

Range Allocation for Separation Logic.

Muralidhar Talupur, Nishant Sinha, Ofer Strichman, Amir Pnueli

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

Validating the Translation of an Industrial Optimizing Compiler.

I. Gordin, Raya Leviathan, Amir Pnueli

Proceedings of the Automated Technology for Verification and Analysis: Second International Conference, 2004

2003

VOC: A Methodology for the Translation Validation of OptimizingCompilers.

Lenore D. Zuck, Amir Pnueli, Benjamin Goldberg

J. Univers. Comput. Sci., 2003

Erratum ("The small model property: how small can it be?" Volume 178, Number 1 [2002], pages 279-293).

Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel

Inf. Comput., 2003

Model-Checking and Abstraction to the Aid of Parameterized Systems.

Amir Pnueli, Lenore D. Zuck

Proceedings of the Verification, 2003

Smart play-out.

David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli

Proceedings of the Companion of the 18th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2003

Parameterized Verification by Probabilistic Abstraction.

Tamarah Arons, Amir Pnueli, Lenore D. Zuck

Proceedings of the Foundations of Software Science and Computational Structures, 2003

Formal Modeling of C. elegans Development: A Scenario-Based Approach.

Na'aman Kam, David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli, E. Jane Albert Hubbard, Michael J. Stern

Proceedings of the Computational Methods in Systems Biology, First International Workshop, 2003

The ROBDD Size of Simple CNF Formulas.

Michael Langberg, Amir Pnueli, Yoav Rodeh

Proceedings of the Correct Hardware Design and Verification Methods, 2003

TLPVS: A PVS-Based LTL Verification System.

Amir Pnueli, Tamarah Arons

Proceedings of the Verification: Theory and Practice, 2003

2002

Complete Proof System for QPTL.

Yonit Kesten, Amir Pnueli

J. Log. Comput., 2002

The Small Model Property: How Small Can It Be?

Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel

Inf. Comput., 2002

Translation and Run-Time Validation of Optimized Code.

Lenore D. Zuck, Amir Pnueli, Yi Fang, Benjamin Goldberg, Ying Hu

Proceedings of the Runtime Verification 2002, 2002

VOC: A Translation Validator for Optimizing Compilers.

Lenore D. Zuck, Amir Pnueli, Yi Fang, Benjamin Goldberg

Proceedings of the Compiler Optimization Meets Compiler Verification, 2002

TimeC: A Time Constraint Language for ILP Processor Compilation.

Allen Leung, Krishna V. Palem, Amir Pnueli

Constraints An Int. J., 2002

Automatic Verification of Probabilistic Free Choice.

Lenore D. Zuck, Amir Pnueli, Yonit Kesten

Proceedings of the Verification, 2002

Applications of Formal Methods in Biology.

Amir Pnueli

Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 2002

Understanding UML: A Formal Semantics of Concurrency and Communication in Real-Time UML.

Werner Damm, Bernhard Josko, Amir Pnueli, Anjelika Votintseva

Proceedings of the Formal Methods for Components and Objects, 2002

Smart Play-out of Behavioral Requirements.

David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli

Proceedings of the Formal Methods in Computer-Aided Design, 4th International Conference, 2002

Embedded Systems: Challenges in Specification and Verification.

Amir Pnueli

Proceedings of the Embedded Software, Second International Conference, 2002

A Deductive Proof System for CTL.

Amir Pnueli, Yonit Kesten

Proceedings of the CONCUR 2002, 2002

Network Invariants in Action.

Yonit Kesten, Amir Pnueli, Elad Shahar, Lenore D. Zuck

Proceedings of the CONCUR 2002, 2002

Liveness with (0, 1, infty)-Counter Abstraction.

Amir Pnueli, Jessie Xu, Lenore D. Zuck

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

Validating software pipelining optimizations.

Raya Leviathan, Amir Pnueli

Proceedings of the International Conference on Compilers, 2002

2001

Scheduling time-constrained instructions on pipelined processors.

Allen Leung, Krishna V. Palem, Amir Pnueli

ACM Trans. Program. Lang. Syst., 2001

Symbolic model checking with rich assertional languages.

Yonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, Elad Shahar

Theor. Comput. Sci., 2001

Verification by Augmented Abstraction: The Automata-Theoretic View.

Yonit Kesten, Amir Pnueli, Moshe Y. Vardi

J. Comput. Syst. Sci., 2001

Automatic Deductive Verification with Invisible Invariants.

Amir Pnueli, Sitvanit Ruah, Lenore D. Zuck

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2001

Sticks and stones: a coding scheme for parameterized verification.

Amir Pnueli

Proceedings of the Twentieth Annual ACM Symposium on Principles of Distributed Computing, 2001

Range Allocation for Equivalence Logic.

Amir Pnueli, Yoav Rodeh, Ofer Strichman

Proceedings of the FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science, 2001

From Falsification to Verification.

Doron A. Peled, Amir Pnueli, Lenore D. Zuck

Proceedings of the FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science, 2001

Beyond Regular Model Checking.

Dana Fisman, Amir Pnueli

Proceedings of the FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science, 2001

Parameterized Verification with Automatically Computed Inductive Assertions.

Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Jiazhao Xu, Lenore D. Zuck

Proceedings of the Computer Aided Verification, 13th International Conference, 2001

2000

Control and Data Abstraction: The Cornerstones of Practical Formal Verification.

Yonit Kesten, Amir Pnueli

Int. J. Softw. Tools Technol. Transf., 2000

Effective synthesis of switching controllers for linear systems.

Eugene Asarin, Olivier Bournez, Thao Dang, Oded Maler, Amir Pnueli

Proc. IEEE, 2000

Propositional Temporal Logics: Decidability and Completeness.

Orna Lichtenstein, Amir Pnueli

Log. J. IGPL, 2000

Verification by Augmented Finitary Abstraction.

Yonit Kesten, Amir Pnueli

Inf. Comput., 2000

Verification of Clocked and Hybrid Systems.

Yonit Kesten, Zohar Manna, Amir Pnueli

Acta Informatica, 2000

A Comparison of Two Verification Methods for Speculative Instruction Execution.

Tamarah Arons, Amir Pnueli

Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 2000

Formal Verification of the Ricart-Agrawala Algorithm.

Ekaterina Sedletsky, Amir Pnueli, Mordechai Ben-Ari

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 2000

Liveness and Acceleration in Parameterized Verification.

Amir Pnueli, Elad Shahar

Proceedings of the Computer Aided Verification, 12th International Conference, 2000

Keynote Address: Abstraction, Composition, Symmetry, and a Little Deduction: The Remedies to State Explosion.

Amir Pnueli

Proceedings of the Computer Aided Verification, 12th International Conference, 2000

Rigorous development of embedded systems.

Amir Pnueli

Proceedings of the 2000 International Conference on Compilers, 2000

1999

Decidable Integration Graphs.

Yonit Kesten, Amir Pnueli, Joseph Sifakis, Sergio Yovine

Inf. Comput., 1999

Proving Refinement Using Transduction.

Bengt Jonsson, Amir Pnueli, Camilla Rump

Distributed Comput., 1999

Verifying Tomasulo's Algoithm by Refinement.

Tamarah Arons, Amir Pnueli

Proceedings of the 12th International Conference on VLSI Design (VLSI Design 1999), 1999

A Framework for Scheduler Synthesis.

Karine Altisen, Gregor Gößler, Amir Pnueli, Joseph Sifakis, Stavros Tripakis, Sergio Yovine

Proceedings of the 20th IEEE Real-Time Systems Symposium, 1999

Orthogonal Polyhedra: Representation and Computation.

Olivier Bournez, Oded Maler, Amir Pnueli

Proceedings of the Hybrid Systems: Computation and Control, Second International Workshop, 1999

A Perfect Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software.

Yonit Kesten, Amit Klein, Amir Pnueli, Gil Raanan

Proceedings of the FM'99 - Formal Methods, 1999

Verifying Liveness by Augmented Abstraction.

Yonit Kesten, Amir Pnueli

Proceedings of the Computer Science Logic, 13th International Workshop, 1999

Deciding Equality Formulas by Small Domains Instantiations.

Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel

Proceedings of the Computer Aided Verification, 11th International Conference, 1999

Translation Validation: From SIGNAL to C.

Amir Pnueli, Ofer Strichman, Michael Siegel

Proceedings of the Correct System Design, 1999

1998

The Code Validation Tool CVT: Automatic Verification of a Compilation Process.

Amir Pnueli, Ofer Strichman, Michael Siegel

Int. J. Softw. Tools Technol. Transf., 1998

Translation Validation.

Amir Pnueli, Michael Siegel, Eli Singerman

Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1998

Modularization and Abstraction: The Keys to Practical Formal Verification.

Yonit Kesten, Amir Pnueli

Proceedings of the Mathematical Foundations of Computer Science 1998, 1998

Translation Validation for Synchronous Languages.

Amir Pnueli, Ofer Strichman, Michael Siegel

Proceedings of the Automata, Languages and Programming, 25th International Colloquium, 1998

Algorithmic Verification of Linear Temporal Logic Specifications.

Yonit Kesten, Amir Pnueli, Li-on Raviv

Proceedings of the Automata, Languages and Programming, 25th International Colloquium, 1998

Fair Synchronous Transition Systems and Their Liveness Proofs.

Amir Pnueli, Natarajan Shankar, Eli Singerman

Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 1998

Verification of Data-Insensitive CIrcuits: An In-Order-Retirement Case Study.

Amir Pnueli, Tamarah Arons

Proceedings of the Formal Methods in Computer-Aided Design, 1998

Translation Validation: From DC+ to C*.

Amir Pnueli, Ofer Strichman, Michael Siegel

Proceedings of the Applied Formal Methods, 1998

Herbrand Automata for Hardware Verification.

Werner Damm, Amir Pnueli, Sitvanit Ruah

Proceedings of the CONCUR '98: Concurrency Theory, 1998

On Discretization of Delays in Timed Automata and Digital Circuits.

Eugene Asarin, Oded Maler, Amir Pnueli

Proceedings of the CONCUR '98: Concurrency Theory, 1998

Deductive vs. Model-Theoretic Approaches to Formal Verification (Abstract of Invited Talk).

Amir Pnueli

Proceedings of the Automated Deduction, 1998

A Fast Algorithm for Scheduling Time-Constrained Instructions on Processors with ILP.

Allen Leung, Krishna V. Palem, Amir Pnueli

Proceedings of the 1998 International Conference on Parallel Architectures and Compilation Techniques, 1998

1997

Verification Engineering: A Future Profession (A. M. Turing Award Lecture).

Amir Pnueli

Proceedings of the Sixteenth Annual ACM Symposium on Principles of Distributed Computing, 1997

Verifying Liveness Properties of Reactive Systems (Tutorial Abstract).

Amir Pnueli

Proceedings of the Hybrid and Real-Time Systems, 1997

Data-Structures for the Verification of Timed Automata.

Eugene Asarin, Marius Bozga, Alain Kerbrat, Oded Maler, Amir Pnueli, Anne Rasse

Proceedings of the Hybrid and Real-Time Systems, 1997

Two Decades of Temporal Logic: Achievements and Challenges (Abstract).

Amir Pnueli

Proceedings of the 38th Annual Symposium on Foundations of Computer Science, 1997

A Compositional Real-Time Semantics of STATEMATE Designs.

Werner Damm, Bernhard Josko, Hardi Hungar, Amir Pnueli

Proceedings of the Compositionality: The Significant Difference, International Symposium, 1997

Verifying out-of-order executions.

Werner Damm, Amir Pnueli

Proceedings of the Advances in Hardware Design and Verification, 1997

Symbolic Model Checking with Rich ssertional Languages.

Yonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, Elad Shahar

Proceedings of the Computer Aided Verification, 9th International Conference, 1997

Some Progress in the Symbolic Verification of Timed Automata.

Marius Bozga, Oded Maler, Amir Pnueli, Sergio Yovine

Proceedings of the Computer Aided Verification, 9th International Conference, 1997

1996

A Platform for Combining Deductive with Algorithmic Verification.

Amir Pnueli, Elad Shahar

Proceedings of the Computer Aided Verification, 8th International Conference, 1996

Using Ghost Variables to Prove Refinement.

Monica Marcus, Amir Pnueli

Proceedings of the Algebraic Methodology and Software Technology, 1996

1995

On the Learnability of Infinitary Regular Sets

Oded Maler, Amir Pnueli

Inf. Comput., May, 1995

Reachability Analysis of Dynamical Systems Having Piecewise-Constant Derivatives.

Eugene Asarin, Oded Maler, Amir Pnueli

Theor. Comput. Sci., 1995

On the Synthesis of Discrete Controllers for Timed Systems (An Extended Abstract).

Oded Maler, Amir Pnueli, Joseph Sifakis

Proceedings of the STACS 95, 1995

Once and For All

Orna Kupferman, Amir Pnueli

Proceedings of the Proceedings, 1995

A Complete Proof Systems for QPTL

Yonit Kesten, Amir Pnueli

Proceedings of the Proceedings, 1995

Verifying Clocked Transition Systems.

Yonit Kesten, Zohar Manna, Amir Pnueli

Proceedings of the Hybrid Systems III: Verification and Control, 1995

Timing analysis of asynchronous circuits using timed automata.

Oded Maler, Amir Pnueli

Proceedings of the Correct Hardware Design and Verification Methods, 1995

Temporal verification of reactive systems - safety.

Zohar Manna, Amir Pnueli

Springer, ISBN: 978-0-387-94459-3, 1995

1994

Temporal Proof Methodologies for Timed Transition Systems

Thomas A. Henzinger, Zohar Manna, Amir Pnueli

Inf. Comput., August, 1994

Proving Partial Order Properties.

Doron A. Peled, Amir Pnueli

Theor. Comput. Sci., 1994

Temporal Verification Diagrams.

Zohar Manna, Amir Pnueli

Proceedings of the Theoretical Aspects of Computer Software, 1994

Compositional Verification of Real-Time Systems

Edward Y. Chang, Zohar Manna, Amir Pnueli

Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), 1994

Symbolic Controller Synthesis for Discrete and Timed Systems.

Eugene Asarin, Oded Maler, Amir Pnueli

Proceedings of the Hybrid Systems II, 1994

Development of Hybrid Systems.

Amir Pnueli

Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, Third International Symposium Organized Jointly with the Working Group Provably Correct Systems, 1994

Prooving Safety Properties of Hybrid Systems.

Arjun Kapur, Thomas A. Henzinger, Zohar Manna, Amir Pnueli

Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, Third International Symposium Organized Jointly with the Working Group Provably Correct Systems, 1994

1993

Probabilistic Verification

Amir Pnueli, Lenore D. Zuck

Inf. Comput., March, 1993

Models for Reactivity.

Zohar Manna, Amir Pnueli

Acta Informatica, 1993

Temporal Verification of Simulation and Refinement.

Yonit Kesten, Zohar Manna, Amir Pnueli

Proceedings of the A Decade of Concurrency, Reflections and Perspectives, 1993

In and Out of Temporal Logic

Amir Pnueli, Lenore D. Zuck

Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS '93), 1993

Reachability Analysis of Planar Multi-limear Systems.

Oded Maler, Amir Pnueli

Proceedings of the Computer Aided Verification, 5th International Conference, 1993

A Decision Algorithm for Full Propositional Temporal Logic.

Yonit Kesten, Zohar Manna, Hugh McGuire, Amir Pnueli

Proceedings of the Computer Aided Verification, 5th International Conference, 1993

Verification of parameterized programs.

Zohar Manna, Amir Pnueli

Proceedings of the Specification and validation methods, 1993

1992

Time for Concurrency.

Zohar Manna, Amir Pnueli

Proceedings of the Future Tendencies in Computer Science, 1992

What Good Are Digital Clocks?

Thomas A. Henzinger, Zohar Manna, Amir Pnueli

Proceedings of the Automata, Languages and Programming, 19th International Colloquium, 1992

Characterization of Temporal Property Classes.

Edward Y. Chang, Zohar Manna, Amir Pnueli

Proceedings of the Automata, Languages and Programming, 19th International Colloquium, 1992

Verifying Hybrid Systems.

Zohar Manna, Amir Pnueli

Proceedings of the Hybrid Systems, 1992

Integration Graphs: A Class of Decidable Hybrid Systems.

Yonit Kesten, Amir Pnueli, Joseph Sifakis, Sergio Yovine

Proceedings of the Hybrid Systems, 1992

Towards Refining Temporal Specifications into Hybrid Systems.

Thomas A. Henzinger, Zohar Manna, Amir Pnueli

Proceedings of the Hybrid Systems, 1992

Timed and Hybrid Statecharts and Their Textual Representation.

Yonit Kesten, Amir Pnueli

Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 1992

System Specification and Refinement in Temporal Logic.

Amir Pnueli

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1992

How Vital is Liveness? Verifying Timing Properties of Reactive and Hybrid Systems (Extended Abstract).

Amir Pnueli

Proceedings of the CONCUR '92, 1992

The temporal logic of reactive and concurrent systems - specification.

Zohar Manna, Amir Pnueli

Springer, ISBN: 978-1-4612-0931-7, 1992

1991

Completing the Temporal Picture.

Zohar Manna, Amir Pnueli

Theor. Comput. Sci., 1991

What is in a Step: On the Semantics of Statecharts.

Amir Pnueli, M. Shalev

Proceedings of the Theoretical Aspects of Computer Software, 1991

From Timed to Hybrid Systems.

Oded Maler, Zohar Manna, Amir Pnueli

Proceedings of the Real-Time: Theory in Practice, 1991

Timed Transition Systems.

Thomas A. Henzinger, Zohar Manna, Amir Pnueli

Proceedings of the Real-Time: Theory in Practice, 1991

Communication with Directed Logic Variables.

Alon Kleinman, Yael Moscowitz, Amir Pnueli, Ehud Shapiro

Proceedings of the Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, 1991

Temporal Proof Methodologies for Real-time Systems.

Thomas A. Henzinger, Zohar Manna, Amir Pnueli

Proceedings of the Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, 1991

On the Faithfulness of Formal Models.

Zohar Manna, Amir Pnueli

Proceedings of the Mathematical Foundations of Computer Science 1991, 1991

Specifying and Proving Serializability in Temporal Logic

Doron A. Peled, Shmuel Katz, Amir Pnueli

Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), 1991

1990

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, Mark B. Trakhtenbrot

IEEE Trans. Software Eng., 1990

A Hierarchy of Temporal Properties.

Zohar Manna, Amir Pnueli

Proceedings of the Ninth Annual ACM Symposium on Principles of Distributed Computing, 1990

Explicit Clock Temporal Logic

Eyal Harel, Orna Lichtenstein, Amir Pnueli

Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), 1990

A temporal proof methodology for reactive systems.

Zohar Manna, Amir Pnueli

Proceedings of the Next Decade in Information Technology: Proceedings of the 5th Jerusalem Conference on Information Technology 1990, 1990

An interleaving model for real-time.

Thomas A. Henzinger, Zohar Manna, Amir Pnueli

Proceedings of the Next Decade in Information Technology: Proceedings of the 5th Jerusalem Conference on Information Technology 1990, 1990

Proving Partial Order Liveness Properties.

Doron A. Peled, Amir Pnueli

Proceedings of the Automata, Languages and Programming, 17th International Colloquium, 1990

Distributed Reactive Systems Are Hard to Synthesize

Amir Pnueli, Roni Rosner

Proceedings of the 31st Annual Symposium on Foundations of Computer Science, 1990

Tight Bounds on the Complexity of Cascaded Decomposition of Automata

Oded Maler, Amir Pnueli

Proceedings of the 31st Annual Symposium on Foundations of Computer Science, 1990

1989

On the Synthesis of a Reactive Module.

Amir Pnueli, Roni Rosner

Proceedings of the Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, 1989

Rooting UNITY.

Rob Gerth, Amir Pnueli

Proceedings of the 5th International Workshop on Software Specification and Design, 1989

Specification and verification of VLSI systems.

Asher Wilk, Amir Pnueli

Proceedings of the 1989 IEEE International Conference on Computer-Aided Design, 1989

On the Synthesis of an Asynchronous Reactive Module.

Amir Pnueli, Roni Rosner

Proceedings of the Automata, Languages and Programming, 16th International Colloquium, 1989

Learning omega-Regular Languages from Queries and Counter-Examples (A Preliminary Report).

Oded Maler, Amir Pnueli

Proceedings of the Analogical and Inductive Inference, 1989

1988

The grammar of dimensions in machine drawings.

Dov Dori, Amir Pnueli

Comput. Vis. Graph. Image Process., 1988

The anchored version of the temporal framework.

Zohar Manna, Amir Pnueli

Proceedings of the Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School/Workshop, Noordwijkerhout, The Netherlands, May 30, 1988

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

Proceedings of the Proceedings, 1988

Applications of Temporal Logic to the Specification of Real-time Systems.

Amir Pnueli, Eyal Harel

Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 1988

A Framework for the Synthesis of Reactive Modules.

Amir Pnueli, Roni Rosner

Proceedings of the Concurrency 88: International Conference on Concurrency, 1988

1987

Very High Level Concurrent Programming.

Yuan Shi, Noah S. Prywes, Boleslaw K. Szymanski, Amir Pnueli

IEEE Trans. Software Eng., 1987

Specification and Verification of Concurrent Programs by forall-Automata.

Zohar Manna, Amir Pnueli

Proceedings of the Temporal Logic in Specification, 1987

Specification and Implementation of Concurrently Accessed Data Structures: An Abstract Data Type Approach.

S. Kaplan, Amir Pnueli

Proceedings of the STACS 87, 1987

A Hierarchy of Temporal Properties (Abstract).

Zohar Manna, Amir Pnueli

Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, 1987

On the Formal Semantics of Statecharts (Extended Abstract)

David Harel, Amir Pnueli, Jeanette P. Schmidt, Rivi Sherman

Proceedings of the Symposium on Logic in Computer Science (LICS '87), 1987

1986

Verification of Multiprocess Probabilistic Protocols.

Amir Pnueli, Lenore D. Zuck

Distributed Comput., 1986

A Really Abstract Concurrent Model and its Temporal Logic.

Howard Barringer, Ruurd Kuiper, Amir Pnueli

Proceedings of the Conference Record of the Thirteenth Annual ACM Symposium on Principles of Programming Languages, 1986

A Choppy Logic

Roni Rosner, Amir Pnueli

Proceedings of the Symposium on Logic in Computer Science (LICS '86), 1986

Probabilistic Verification by Tableaux

Amir Pnueli, Lenore D. Zuck

Proceedings of the Symposium on Logic in Computer Science (LICS '86), 1986

Specification and Development of Reactive Systems (Invited Paper).

Amir Pnueli

Proceedings of the Information Processing 86, 1986

Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends.

Amir Pnueli

Proceedings of the Current Trends in Concurrency, Overviews and Tutorials, 1986

1985

Checking That Finite State Concurrent Programs Satisfy Their Linear Specification.

Orna Lichtenstein, Amir Pnueli

Proceedings of the Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, 1985

The Glory of the Past.

Orna Lichtenstein, Amir Pnueli, Lenore D. Zuck

Proceedings of the Logics of Programs, 1985

Proving Termination of Prolog Programs.

Nissim Francez, Orna Grumberg, Shmuel Katz, Amir Pnueli

Proceedings of the Logics of Programs, 1985

Linear and Branching Structures in the Semantics and Logics of Reactive Systems.

Amir Pnueli

Proceedings of the Automata, 1985

1984

Automatic program generation in distributed cooperative computation.

Noah S. Prywes, Amir Pnueli

IEEE Trans. Syst. Man Cybern., 1984

A Linear-History Semantics for Languages for Distributed Programming.

Nissim Francez, Daniel Lehmann, Amir Pnueli

Theor. Comput. Sci., 1984

Symmetric and Economical Solutions to the Mutual Exclusion Problem in a Distributed System.

Shimon Cohen, Daniel Lehmann, Amir Pnueli

Theor. Comput. Sci., 1984

Fair Termination Revisited-With Delay.

Krzysztof R. Apt, Amir Pnueli, Jonathan Stavi

Theor. Comput. Sci., 1984

Is the Interesting Part of Process Logic Uninteresting? A Translation from PL to PDL.

Rivi Sherman, Amir Pnueli, David Harel

SIAM J. Comput., 1984

Verification of Probabilistic Programs.

Micha Sharir, Amir Pnueli, Sergiu Hart

SIAM J. Comput., 1984

Adequate Proof Principles for Invariance and Liveness Properties of Concurrent Programs.

Zohar Manna, Amir Pnueli

Sci. Comput. Program., 1984

Now You May Compose Temporal Logic Specifications

Howard Barringer, Ruurd Kuiper, Amir Pnueli

Proceedings of the 16th Annual ACM Symposium on Theory of Computing, April 30, 1984

Temporal Verification of Carrier-Sense Local Area Network Protocols.

Dennis E. Shasha, Amir Pnueli, W. Ewald

Proceedings of the Conference Record of the Eleventh Annual ACM Symposium on Principles of Programming Languages, 1984

In Transition From Global to Modular Temporal Reasoning about Programs.

Amir Pnueli

Proceedings of the Logics and Models of Concurrent Systems, 1984

On the Development of Reactive Systems.

David Harel, Amir Pnueli

Proceedings of the Logics and Models of Concurrent Systems, 1984

A Hardware Implementation of the CSP Primitives and its Verification.

Dorit Ron, Flavia Rosemberg, Amir Pnueli

Proceedings of the Automata, 1984

On the scope of static checking in definitional languages.

Boleslaw K. Szymanski, Noah S. Prywes, Evan D. Lock, Amir Pnueli

Proceedings of the 1984 ACM Annual Conference on Computer Science: The fifth generation challenge, 1984

1983

Compilation of Nonprocedural Specifications into Computer Programs.

Noah S. Prywes, Amir Pnueli

IEEE Trans. Software Eng., 1983

Termination of Probabilistic Concurrent Program.

Sergiu Hart, Micha Sharir, Amir Pnueli

ACM Trans. Program. Lang. Syst., 1983

Propositional Dynamic Logic of Nonregular Programs.

David Harel, Amir Pnueli, Jonathan Stavi

J. Comput. Syst. Sci., 1983

The Temporal Logic of Branching Time.

Mordechai Ben-Ari, Amir Pnueli, Zohar Manna

Acta Informatica, 1983

On the Extremely Fair Treatment of Probabilistic Algorithms

Amir Pnueli

Proceedings of the 15th Annual ACM Symposium on Theory of Computing, 1983

How to Cook a Temporal Proof System for Your Pet Language.

Zohar Manna, Amir Pnueli

Proceedings of the Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, 1983

There Exit Decidable Context Free Propositional Dynamic Logics.

Tmima Koren, Amir Pnueli

Proceedings of the Logics of Programs, 1983

Proving Precedence Properties: The Temporal Way.

Zohar Manna, Amir Pnueli

Proceedings of the Automata, 1983

Symmetric and Economical Solutions to the Mutual Exclusion Problem in a Distributed System (Extended Abstract).

Shimon Cohen, Daniel Lehmann, Amir Pnueli

Proceedings of the Automata, 1983

Solutions to Problem No.2.

Amir Pnueli

Proceedings of the Analysis of Concurrent Systems, 1983

1982

Deterministic Propositional Dynamic Logic: Finite Models, Complexity, and Completeness.

Mordechai Ben-Ari, Joseph Y. Halpern, Amir Pnueli

J. Comput. Syst. Sci., 1982

Termination of Probabilistic Concurrent Programs.

Sergiu Hart, Micha Sharir, Amir Pnueli

Proceedings of the Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages, 1982

Rendezvous with ADA: a proof theoretical view.

Amir Pnueli, Willem P. de Roever

Proceedings of the AdaTEC Conference on Ada, 1982

1981

The Temporal Semantics of Concurrent Programs.

Amir Pnueli

Theor. Comput. Sci., 1981

Automatic Programming of Finite State Linear Programs.

Amir Pnueli, Giora Slutzki

SIAM J. Comput., 1981

Verification of Concurrent Programs: Temporal Proof Principles.

Zohar Manna, Amir Pnueli

Proceedings of the Logics of Programs, Workshop, Yorktown Heights, New York, USA, May 1981, 1981

Further Results on Propositional Dynamic Logic of Nonregular Programs.

David Harel, Amir Pnueli, Jonathan Stavi

Proceedings of the Logics of Programs, Workshop, Yorktown Heights, New York, USA, May 1981, 1981

Realizing an Equational Specification.

Amir Pnueli, R. Zarhi

Proceedings of the Automata, 1981

Impartiality, Justice and Fairness: The Ethics of Concurrent Termination.

Daniel Lehmann, Amir Pnueli, Jonathan Stavi

Proceedings of the Automata, 1981

Finite Models for Deterministic Propositional Dynamic Logic.

Mordechai Ben-Ari, Joseph Y. Halpern, Amir Pnueli

Proceedings of the Automata, 1981

Propositional Dynamic Logic of Context-Free Programs

David Harel, Amir Pnueli, Jonathan Stavi

Proceedings of the 22nd Annual Symposium on Foundations of Computer Science, 1981

1980

Synchronous Schemes and Their Decision Problems.

Zohar Manna, Amir Pnueli

Proceedings of the Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, 1980

On the Temporal Analysis of Fairness.

Dov M. Gabbay, Amir Pnueli, Saharon Shelah, Jonathan Stavi

Proceedings of the Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, 1980

A Linear History Semantics for Distributed Languages (Extended Abstract)

Nissim Francez, Daniel Lehmann, Amir Pnueli

Proceedings of the 21st Annual Symposium on Foundations of Computer Science, 1980

1979

Use of a Nonprocedural Specification Language and Associated Program Generator in Software Development.

Noah S. Prywes, Amir Pnueli, S. Shastry

ACM Trans. Program. Lang. Syst., 1979

The Modal Logic of Programs.

Zohar Manna, Amir Pnueli

Proceedings of the Automata, 1979

1978

A Proof Method for Cyclic Programs.

Nissim Francez, Amir Pnueli

Acta Informatica, 1978

1977

A Direct Algorithm for Checking Equivalence of LL<i>(k)</i> Grammars.

Tmima Olshansky, Amir Pnueli

Theor. Comput. Sci., 1977

Backtracking in Recursive Computations.

Nissim Francez, Boris Klebansky, Amir Pnueli

Acta Informatica, 1977

A Complete Axiomatic System for Proving Deductions about Recursive Programs

David Harel, Amir Pnueli, Jonathan Stavi

Proceedings of the 9th Annual ACM Symposium on Theory of Computing, 1977

Simple Programs and Their Decision Problems.

Amir Pnueli, Giora Slutzki

Proceedings of the Automata, 1977

The Temporal Logic of Programs

Amir Pnueli

Proceedings of the 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October, 1977

1974

Axiomatic Approach to Total Correctness of Programs.

Zohar Manna, Amir Pnueli

Acta Informatica, 1974

1973

Decidable Properties of Monadic Functional Schemas.

Edward A. Ashcroft, Zohar Manna, Amir Pnueli

J. ACM, 1973

1972

Permutation Graphs and Transitive Graphs.

Shimon Even, Amir Pnueli, Abraham Lempel

J. ACM, 1972

1971

Marked Directed Graphs.

Frederic G. Commoner, Anatol W. Holt, Shimon Even, Amir Pnueli

J. Comput. Syst. Sci., 1971

1970

Formalization of Properties of Functional Programs.

Zohar Manna, Amir Pnueli

J. ACM, 1970

1969

Formalization of Properties of Recursively Defined Functions

Zohar Manna, Amir Pnueli

Proceedings of the 1st Annual ACM Symposium on Theory of Computing, 1969