Conferences and Journals

• T. Arons, A. Pnueli, and L. Zuck. Parameterized verification by probabilistic abstraction. In Proceedings 6^th International Conference on Foundations of Software Science and Computational Structures, volume 2620 of Lecture Notes in Computer Science, pages 87-102, Warsaw, Poland, April 2003. © Springer-Verlag. (Gzipped PostScript, 16 pages, 126112 bytes) (PDF, 230017 bytes)

• N. Kam, D. Harel, H. Kugler, R. Marelly, A. Pnueli, J. Hubbard, and M. Stern. Formal modeling of c. elegans development: A scenario-based approach. In First International Workshop on Computational Methods in Systems Biology, volume 2602 of Lecture Notes in Computer Science, pages 4-20, Rovereto, Italy, February 2003. © Springer-Verlag. (PDF, 240844 bytes)

• Y. Kesten, N. Piterman, and A. Pnueli. Bridging the gap between fair simulation and trace inclusion. In Proceedings of 15^th International Conference on Computer Aided Verification, volume 2775 of Lecture Notes in Computer Science, pages 381-393, Boulder, CO, USA, July 2003. © Springer-Verlag. (Gzipped PostScript, 21 pages, 97297 bytes) (PDF, 281026 bytes)

• M. Langberg, A. Pnueli, and Y. Rodeh. The robdd size of simple cnf formulas. In proceedings 12^th Advanced Research Working Conference on Correct Hardware Design and Verification Methods, Lecture Notes in Computer Science, pages 363-377, L'Aquila, Italy, October 2003. © Springer-Verlag. (Gzipped PostScript, 15 pages, 112182 bytes) (PDF, 263285 bytes)

• L. Zuck, A. Pnueli, and Y. Kesten. Automatic verification of free choice. In Proc. of the 3rd workshop on Verification, Model Checking, and Abstract Interpretation, volume 2294 of Lecture Notes in Computer Science, pages 208-224, Venice, Italy, January 2002. © Springer-Verlag. (Gzipped PostScript, 16 pages, 96771 bytes) (PDF, 259502 bytes)

• D. Harel, H. Kugler, R. Marelly, and A. Pnueli. Smart play-out of behavioral requirements. Technical Report MCS02-08, Weizmann Institute of Science, April 2002. (Gzipped PostScript, 21 pages, 218812 bytes) (PDF, 201050 bytes)

• A. Leung, K. V. Palem, and Amir Pnueli. TimeC: A time constraint language for ilp processor compilation. Constraints, 7(2):75-115, April 2002.

• L. Zuck, A. Pnueli, Y. Fang, B. Goldberg, and Y. Hu. Translation and run-time validation of optimized code. In 2nd Workshop on Runtime Verification, volume 70(4) of Electronic Notes in Theoretical Computer Science, pages 180-201, Copenhagen, Denmark, July 2002. Elsevier Science. (PostScript)

• A. Pnueli, J. Xu, and L. Zuck. Liveness with (0,1,infinity)-counter abstraction. In 14th. International Conference on Computer Aided Verification, volume 2404 of Lecture Notes in Computer Science, pages 107-122, Copenhagen, Denmark, July 2002. © Springer-Verlag. (Gzipped PostScript, 18 pages, 132471 bytes)

• Y. Kesten, A. Pnueli, E. Shahar, and L. Zuck. Network invariants in action. In Proc. 13th Conference on Concurrency Theory, volume 2421 of Lecture Notes in Computer Science, pages 101-115, Brno, Czech Republic, August 2002. © Springer-Verlag. (Gzipped PostScript, 15 pages, 104557 bytes) (PDF, 258666 bytes)

• A. Pnueli and Y. Kesten. A deductive proof system for CTL*. In Proc. 13th Conference on Concurrency Theory, volume 2421 of Lecture Notes in Computer Science, pages 24-40, Brno, Czech Republic, August 2002. © Springer-Verlag. (Gzipped PostScript, 17 pages, 105358 bytes) (PDF, 249562 bytes)

• R. Leviathan and A. Pnueli. Validating software pipelining optimizations. In Proc. International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, volume 314, pages 280-287, Grenoble, France, October 2002. ACM, © ACM. (Gzipped PostScript, 8 pages, 147719 bytes) (PDF, 155039 bytes)

• A. Pnueli, Y. Rodeh, O. Strichman, and M. Siegel. The small model property: How small can it be? Information and Computation, 178(1):279-293, October 2002. (PostScript)

• D. Harel, H. Kugler, R. Marelly, and A. Pnueli. Smart play-out of behavioral requirements. In 4th International Conference on Formal Methods in Computer-Aided Design, volume 2517 of Lecture Notes in Computer Science, pages 378-398, Portland, Oregon, USA, November 2002. © Springer-Verlag. (Springer PDF)

• Y. Kesten and A. Pnueli. Complete proof system for QPTL. Journal of Logic and Computation, 12(5):701-745, December 2002. (Gzipped PostScript, 51 pages, 209633 bytes) (PDF, 561383 bytes)

• A. Leung, K. Palem, and A. Pnueli. Scheduling time-constrained instructions on pipelined processors. ACM Transactions on Programming Languages and Systems, 23(1):73-103, January 2001. (PostScript)

• T. Arons and A. Pnueli. A methodology for deductive verification of out-of-order execution systems based on predicted values. Technical Report MCS01-04, Weizmann Institute of Science, February 2001. (Gzipped PostScript, 16 pages, 94456 bytes)

• A. Pnueli, Y. Rodeh, and O. Strichman. Finite instantiations in equivalence logic with uninterpreted functions. Technical report, Weizmann Institute of Science, 2001. (Gzipped PostScript, 22 pages, 118008 bytes) (PDF, 272518 bytes)

• Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. Theoretical Computer Science, 256:93-112, April 2001. (Gzipped PostScript, 25 pages, 136882 bytes) (PDF, 296508 bytes)

• A. Pnueli, S. Ruah, and L. Zuck. Automatic deductive verification with invisible invariants. In Tools and Algorithms for the Analysis and Construction of Systems, volume 2031 of Lecture Notes in Computer Science, pages 82-97, Genova, Italy, April 2001. ETAPS, © Springer. (Gzipped PostScript, 16 pages, 110084 bytes) (PDF, 265592 bytes)

• Y. Kesten, A. Pnueli, and M. Vardi. Verification by augmented abstraction : The automata theoretic view. Journal of Computer and System Sciences , 62(4):668-690, June 2001. (Gzipped PostScript, 26 pages, 166116 bytes) (PDF, 3995077 bytes)

• T. Arons, A.Pnueli, S.Ruah, J.Xu, and L.Zuck. Parameterized verification with automatically computed inductive assertions. In 13th International Conference on Computer Aided Verification, volume 2102 of Lecture Notes in Computer Science, pages 221-234, Paris, France, July 2001. © Springer-Verlag. (Gzipped PostScript, 13 pages, 110152 bytes) (PDF, 294518 bytes)

• L. Zuck, A. Pnueli, and R. Leviathan. Validation of optimizing compilers. Technical Report MCS01-12, Weizmann Institute of Science, August 2001. (Gzipped PostScript, 13 pages, 284260 bytes) (PDF, 320181 bytes)

• R. Leviathan and A. Pnueli. Validating software pipelining optimizations. Technical Report MCS01-11, Weizmann Institute of Science, August 2001. (Gzipped PostScript, 13 pages, 108123 bytes) (PDF, 202537 bytes)

• A. Pnueli, Y. Rodeh, and O. Strichman. Range allocation for equivalence logic. In Proc. 21st conference on Foundations of Software Technology and Theoretical Computer Science, volume 2245 of Lecture Notes in Computer Science, pages 317-333, Bangalore, India, December 2001. © Springer-Verlag. (Gzipped PostScript, 14 pages, 113740 bytes) (PDF, 230343 bytes)

• D. Peled, A. Pnueli, and L. Zuck. From falsification to verification. In Proc. 21st conference on Foundations of Software Technology and Theoretical Computer Science, volume 2245 of Lecture Notes in Computer Science, pages 292-304, Bangalore, India, December 2001. © Springer-Verlag. (Gzipped PostScript, 14 pages, 96769 bytes) (PDF, 220645 bytes)

• D. Fisman and A. Pnueli. Beyond regular model checking. In Proc. 21st conference on Foundations of Software Technology and Theoretical Computer Science, volume 2245 of Lecture Notes in Computer Science, pages 156-170, Bangalore, India, December 2001. © Springer-Verlag. (Gzipped PostScript, 26 pages, 147781 bytes) (PDF, 349128 bytes)

• O. Lichtenstein and A. Pnueli. Propositional temporal logics: Decidability and completeness. Logic Journal of the IGPL, 8(1):55-85, 2000. (Gzipped PostScript, 31 pages, 146539 bytes)

• A. Pnueli, O. Shtrichman, and M. Siegel. Translation validation: From signal to c. In Correct System Design Recent Insights and Advances, volume 1710 of Lecture Notes in Computer Science, pages 231-255. © Springer, March 2000. (Gzipped PostScript, 25 pages, 129250 bytes) (PDF, 302749 bytes)

• Y. Kesten and A. Pnueli. Control and data abstractions: The cornerstones of formal verification. International Journal on Software Tools for Technology Transfer (STTT), 2(1):328-342, 2000. (Gzipped PostScript, 40 pages, 204861 bytes) (PDF, 6476972 bytes)

• T. Arons and A. Pnueli. A comparison of two verification methods for speculative instruction execution. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000), number 1785 in Lecture Notes in Computer Science, pages 487-502, Berlin, Germany, March 2000. © Springer-Verlag. (Gzipped PostScript, 15 pages, 89001 bytes) (PDF, 220148 bytes) (PVS dump files)

• E. Asarin, O. Bournez, T. Dang, O. Maler, and A. Pnueli. Effective synthesis of switching controllers for linear systems. Proceedings of the IEEE, 88(7):1011-1025, July 2000. (PDF)

• Y. Kesten, Z. Manna, and A. Pnueli. Verification of clocked and hybrid systems. Acta Informatica, 36(11):836-912, 2000. (Gzipped PostScript, 74 pages, 271058 bytes) (PDF, 10902198 bytes)

• A. Pnueli and E. Shahar. Liveness and acceleration in parameterized verification. In Computer Aided Verification, volume 1855 of Lecture Notes in Computer Science, pages 328-343. © Springer-Verlag, July 2000. (Gzipped PostScript, 16 pages, 100687 bytes) (PDF, 241435 bytes)

• E. Sedletsky, A. Pnueli, and M. Ben-Ari. Formal verification of the ricart-agrawala algorithm. In Proc. 20th Conference on the Foundations of Software Technology and Theoretical Computer Science, volume 1974 of Lecture Notes in Computer Science, pages 325-335. © Springer-Verlag, December 2000. (PDF, 188124 bytes)

• T. Arons and A. Pnueli. Verifying Tomasulo's algorithm by refinement. In The Twelfth International Conference on VLSI Design, pages 306-309, Goa, India, January 1999. IEEE Computer Society. (Gzipped PostScript, 4 pages, 25211 bytes) (PVS dump file)

• O. Bournez, O. Maler, and A. Pnueli. Orthogonal polyhedra: Representation and computation. In 2nd International Workshop on Hybrid Systems: Computation and Control, volume 1569 of Lecture Notes in Computer Science , Berg en Dal, The Netherlands, March 1999. © Springer-Verlag. ( Springer PDF)

• Y. Kesten, A. Pnueli, J. Sifakis, and S. Yovine. Decidable integration graphs. Information and Computation, 150(2):209-243, May 1999. (I&C PDF)

• B. Jonsson, A. Pnueli, and C. Rump. Proving refinement using transduction. Distributed Computing, 12(2-3):129-149, June 1999. (Springer PDF)

• A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel. Deciding equality formulas by small domains instantiations. In Proc. 11th International Computer Aided Verification Conference, volume 1633 of Lecture Notes in Computer Science , pages 455-469. © Springer-Verlag, July 1999. (Gzipped PostScript, 12 pages, 102355 bytes)

• Y. Kesten, A. Klein, A. Pnueli, and G. Raanan. Bridging the e-business gap through formal verification. In M. Hinchey and J. Bowen, editors, Industrial-Strength Formal Methods in Practice, Formal Approaches to Computing and Information Technology, chapter 6, pages 117-137. © Springer-Verlag, September 1999.

• Y. Kesten, A. Klein, A. Pnueli, and G. Raanan. A perfecto verification: Combining model checking with deductive analysis to verify real-life software. In Formal Methods, Volume I, volume 1708 of Lecture Notes in Computer Science , pages 173-194, Toulouse, France, September 1999. © Springer-Verlag. (Springer PDF)

• A. Pnueli. Deduction is forever. An invited talk at "Formal Methods", Toulouse, September 1999.

• Y. Kesten and A. Pnueli. Verifying liveness by augmented abstraction. In Computer Science Logic, 13th International Workshop, volume 1683 of Lecture Notes in Computer Science, pages 141-156. © Springer-Verlag, September 1999.

• K. Altisen, G. Gossler, A. Pnueli, J. Sifakis, S. Tripakis, and S. Yovine. A framework for scheduler synthesis. In Proc. 20th IEEE Real-Time Systems Symposium, pages 154-163, Phoenix, AZ, USA, December 1999. IEEE, IEEE Computer Society Press. (IEEE PDF)

• A. Pnueli, O. Shtrichman, and M. Siegel. The code validation tool cvt: Automatic verification of a compilation process. International Journal on Software Tools for Technology Transfer (STTT), 2(1):192-201, 1998. (Gzipped PostScript, 10 pages, 127055 bytes)

• A. Pnueli, E. Asarin, O. Maler, and J.Sifakis. Controller synthesis for timed automata. In 5th IFAC conference on System Structure and Control, IFAC Proceedings Volumes, pages 469-474, Nantes, France, July 1998. IFAC, Elsevier.

• A. Pnueli, M. Siegel, and O. Shtrichman. The code validation tool (cvt) - automatic verification of code generated from synchronous languages. In Proc. of the intl. workshop of Software Tools for Technology Transfer, volume NS-98-4 of BRICS notes series, pages 7-12, Aalborg, Denmark, July 1998. BRICS. (Gzipped PostScript, 106710 bytes)

• W. Damm, B. Josko, H. Hungar, and A. Pnueli. A compositional real-time semantics of STATEMATE designs. In International Symposium Compositionality: The Significant Difference, volume 1536 of Lecture Notes in Computer Science , pages 186-238, Bad Malente, Germany, September 1998. © Springer-Verlag. ( Springer PDF)

• A. Pnueli and T. Arons. Verification of data-insensitive circuits: An in-order-retirement case study. In Formal Methods in Computer-Aided Design (FMCAD '98), volume 1522 of Lecture Notes in Computer Science , pages 351-368, Palo Alto, CA, November 1998. © Springer-Verlag. (Gzipped PostScript, 18 pages, 102959 bytes) (PVS dump file)

• A. Pnueli, O. Shtrichman, and M. Siegel. Translation validation: From dc+ to c*. In International Workshop on Current Trends in Applied Formal Methods, volume 1641 of Lecture Notes in Computer Science, pages 137-150, Boppard, Germany, October 1998. © Springer-Verlag.

• A. Leung, K.V. Palem, and A. Pnueli. A Fast Algorithm for Scheduling Time-Constrained Instructions on Processors with ILP. In The 1998 International Conference on Parallel Architectures and Compilation Techniques (PACT 98), Paris, October, 1998. [Abstract+PostScript]
• A. Leung, K.V. Palem, and A. Pnueli. TimeC: A Time Constraint Language for ILP Processor Compilation. In The 5th Annual Australasian Conference on Parallel and Real-Time Systems (PART 98), Adelaide, Australia, September, 1998. [Abstract+PostScript]
• A. Pnueli, N. Shankar, and E. Singerman. Fair Synchronous Transition Systems and their Liveness Proofs. In A.P. Ravn and H. Rischel, editors, 5th International School and Symposium on Formal Techniques in Real-time and Fault-tolerant Systems (FTRTFT 98), Lecture Notes in Computer Science. Springer-Verlag, 1998. [Abstract+PostScript]
• W. Damm, A. Pnueli, and S. Ruah. Herbrand Automata for Hardware Verification. In R. De Simone and D. Sangiorgi, editors, Proceedings of the 9th International Conference on Concurrency (CONCUR 1998), Lecture Notes in Computer Science. Springer-Verlag, 1998. [Abstract+PostScript]
• E. Asarin, O. Maler, and A. Pnueli. On Discretization of Delays in Timed Automata and Digital Circuits. In R. De Simone and D. Sangiorgi, editors, Proceedings of the 9th International Conference on Concurrency (CONCUR 1998), Lecture Notes in Computer Science. Springer-Verlag, 1998.

• Y. Kesten, and A. Pnueli. Modularization and Abstraction: The Keys to Formal Verification. In L. Brim, J. Gruska, and J. Zlatuska, editors, The 23rd International Symposium on Mathematical Foundations of Computer Science (MFCS 1998), volume 1450 of Lecture Notes in Computer Science, pages 54-71. Springer-Verlag, 1998. [Abstract+PostScript]
• Y. Kesten, A. Pnueli, and L. Raviv. Algorithmic Verification of Linear Temporal Logic Specifications. In K.G. Larsen, S. Skyum, and G. Winskel, editors, Proceedings of the 25th International Colloquium on Automata, Languages, and Programming (ICALP 1998), volume 1443 of Lecture Notes in Computer Science, pages 1-16. Springer-Verlag, 1998. [PostScript]
• A. Pnueli, M. Siegel, and O. Shtrichman. Translation Validation for Synchronous Languages. In K.G. Larsen, S. Skyum, and G. Winskel, editors, Proceedings of the 25th International Colloquium on Automata, Languages, and Programming (ICALP 1998), volume 1443 of Lecture Notes in Computer Science, pages 235-246. Springer-Verlag, 1998. [Abstract+PostScript]
• A. Pnueli, M. Siegel, and E. Singerman. Translation Validation. In B. Steffen, editor, Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 1998), volume 1384 of Lecture Notes in Computer Science, pages 151-166. Springer-Verlag, 1998.

• Y. Kesten, Z.  Manna, and A. Pnueli. Verification of Clocked and Hybrid Systems. In G. Rozenberg and F.W. Vaandrager, editors, Lectures on Embedded Systems, volume 1494 of Lecture Notes in Computer Science, pages 4-73. Springer-Verlag, 1998. [PostScript]
• W. Damm, and A. Pnueli. Verifying Out-of-Order Executions. In H.F. Li and D.K. Probst, editors, Advances in Hardware Design and Verification: IFIP WG 10.5 Internatinal Conference on Correct Hardware Design and Verification Methods (CHARME), pages 23-47, Montreal, 1997. Chapmann & Hall.

• M. Bozga, O. Maler, A. Pnueli, and S. Yovine. Some Progress in the Symbolic Verification of Timed Automata. In O. Grumberg, editor, Proceedings of the 9th International Conference on Computer Aided Verification (CAV 1997), Lecture Notes in Computer Science, pages 179-190. Springer-Verlag, 1997.

• Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic Model Checking with Rich Assertional Languages. In O. Grumberg, editor, Proceedings of the 9th International Conference on Computer Aided Verification (CAV 1997), Lecture Notes in Computer Science, pages 424-435. Springer-Verlag, 1997.

• E. Asarin, M. Bozga, A. Kerbrat, O. Maler, A. Pnueli, and A.Rasse. Data-Structures for the Verification of Timed Automata. In O. Maler, editor, Proc. HART'97, volume 1201 of Lecture Notes in Computer Science, pages 346-360. Springer-Verlag, 1997.

• A. Pnueli, and E. Shahar. A Platform for Combining Deductive with Algorithmic Verification. In R. Alur and T. Henzinger, editors, Proceedings of the 8th International Conference on Computer Aided Verification (CAV 1996), Lecture Notes in Computer Science, pages 184-195. Springer-Verlag, 1996.

• Z. Manna, and A. Pnueli. Clocked Transition Systems. In A. Pnueli and H. Lin, editors, Logic and Software Engineering, pages 3 -- 42. World Scientific, Singapore, 1996.

• M. Marcus, and A. Pnueli. Using Ghost Variables to Prove Refinement. In Proceedings of the Fifth International Conference on Algebraic Methodology and Software Technology (AMAST'96), volume 1101 of Lecture Notes in Computer Science, pages 226-240. Springer-Verlag, 1996.

• Y. Kesten, Z. Manna, and A. Pnueli. Verifying Clocked Transition Systems. In R. Alur, T.A. Henzinger, and E.D. Sontag, editors, Hybrid Systems III, volume 1066 of Lecture Notes in Computer Science, pages 13-40. Springer-Verlag, 1996.

• E. Asarin, O. Maler, and A. Pnueli. Reachability Analysis of Dynamical Systems having Piecewise-Constant Derivatives. Theoretical Computer Science, 138(1):35-66, 1995. Special issue on Hybrid Systems.

• O. Maler, and A. Pnueli. On the Learnability of Infinitary Regular Sets. Information and Computation, 118:316-326, 1995.

• O. Kupferman, and A. Pnueli. Once and For All. In Proceedings of the 10th IEEE Symposium Logic in Computer Science (LICS 1995), pages 25-35, 1995.

• Z. Manna, and A. Pnueli. Verification of Parameterized Programs. In E. Börger, editor, Specification and Validation Methods, pages 167-230. Oxford University Press, Oxford, 1995.

• Y. Kesten, and A. Pnueli. A Complete Axiomatization of QPTL. In Proceedings of the 10th IEEE Symposium Logic in Computer Science (LICS 1995), pages 2-12, 1995.

• O. Maler, and A. Pnueli. Timing Analysis of Asynchronous Circuits using Timed Automata. In P. Camurati and H. Eveking, editors, Proc. CHARME'95, volume 987 of Lecture Notes in Computer Science, pages 189-205. Springer-Verlag, 1995.

• O. Maler, A. Pnueli, and J. Sifakis. On the Synthesis of Discrete Controllers for Timed Systems. In E.W. Mayr and C. Puech, editors, Proceedings of STACS'95, volume 900 of Lecture Notes in Computer Science, pages 229-242. Springer-Verlag, 1995. [Abstract and Postscript]
• E. Asarin, O. Maler, and A. Pnueli. Symbolic Controller Synthesis for Discrete and Timed Systems. In P. Antsaklis, W. Kohn, A. Nerode, and S. Sastry, editors, Hybrid System II, volume 999 of Lecture Notes in Computer Science. Springer-Verlag, 1995. [Abstract and Postscript]
• D. Peled, and A. Pnueli. Proving Partial Order Properties. Theoretical Computer Science, 126, 1994.

• T. Henzinger, Z. Manna, and A. Pnueli. Temporal Proof Methodologies for Timed Transition Systems. Information and Computation, 112(2):273-337, 1994.

• E.S. Chang, Z. Manna, and A. Pnueli. Compositional Verification of Real-time Systems. In Proceedings of the 9th IEEE Symposium Logic in Computer Science (LICS 1994), pages 458-465. IEEE Computer Society Press, 1994.

• E. Chang, Z. Manna, and A. Pnueli. Compositional Verification of Real-Time Systems. In Proceedings of the 9th IEEE Symposium Logic in Computer Science (LICS 1994), pages 458-465, 1994.

• Y. Kesten, Z. Manna, and A. Pnueli. Temporal Verification of Simulation and Refinement. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, A Decade of Concurrency, volume 803 of Lecture Notes in Computer Science, pages 273-346. Springer-Verlag, 1994.

• A. Kapur, T.A. Henzinger, Z. Manna, and A. Pnueli. Proving Safety Properties of Hybrid Systems. In H. Langmaack, W.-P. de Roever, and J. Vytopil, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 863 of Lecture Notes in Computer Science, pages 431-454. Springer-Verlag, 1994.

• Z. Manna, and A. Pnueli. Temporal Verification Diagrams. In T. Ito and A. R. Meyer, editors, Theoretical Aspects of Computer Software, volume 789 of Lecture Notes in Computer Science, pages 726-765. Springer-Verlag, 1994.

• Z. Manna, and A. Pnueli. Models for Reactivity. Acta Informatica, 30:609-678, 1993.

• A. Pnueli, and L.D. Zuck. Probabilistic Verification. Information and Computation, 103(1):1-29, 1993.

• A. Pnueli, and L. Zuck. In and Out of Temporal Logic. In Proceedings of the 8th IEEE Symposium Logic in Computer Science (LICS 1993), pages 124-135, 1993.

• Z. Manna, and A. Pnueli. A Temporal Proof Methodology for Reactive Systems. In M. Broy, editor, Program Design Calculi, volume 118 of NATO ASI Series, Series F: Computer and System Sciences, pages 287-323. Springer-Verlag, 1993.

• Z. Manna, and A. Pnueli. Verifying Hybrid Systems. In R.L. Grossman, A. Nerode, A. Ravn, and H. Rischel, editors, Hybrid Systems, volume 736 of Lecture Notes in Computer Science, pages 4-35. Springer-Verlag, 1993.

• O. Maler, and A. Pnueli. Reachability Analysis of Planar Multi-linear Systems. In C. Courcoubetis, editor, Proc. 5th Workshop on Computer Aided Verification, volume 697 of Lecture Notes in Computer Science, pages 194-209. Springer-Verlag, 1993.

• Y. Kesten, A. Pnueli, J. Sifakis, and S. Yovine. Integration Graphs: A Class of Decidable Hybrid Systems. In R.L. Grossman, A. Nerode, A. Ravn, and H. Rischel, editors, Hybrid Systems, volume 736 of Lecture Notes in Computer Science, pages 179-208. Springer-Verlag, 1993.

• Y. Kesten, Z. Manna, H. McGuire, and A. Pnueli. A Decision Algorithm for Full Propositional Temporal Logic. In C. Courcoubetis, editor, Proceedings of the 5th International Conference on Computer Aided Verification (CAV 1993), volume 697 of Lecture Notes in Computer Science, pages 97-109. Springer-Verlag, 1993.

• T. Henzinger, Z. Manna, and A. Pnueli. Towards Refining Temporal Specifications into Hybrid Systems. In R.L. Grossman, A. Nerode, A. Ravn, and H. Rischel, editors, Hybrid Systems, volume 736 of Lecture Notes in Computer Science, pages 60-76. Springer-Verlag, 1993.

• A. Pnueli. System Specification and Refinement in Temporal Logic. In R.K. Shyamasundar, editor, Foundations of Software Technology and Theoretical Computer Science, volume 652 of Lecture Notes in Computer Science, pages 1-38. Springer-Verlag, 1992.

• E.S. Chang, Z. Manna, and A. Pnueli. The Safety-Progress Classification. In sub-series F: Computer and System Science, NATO Advanced Science Institutes Series. Springer-Verlag, 1992.

• Z. Manna, and A. Pnueli. Time for Concurrency. In A. Bensoussan and J.-P. Verjus, editors, Future Tendencies in Computer Science, Control and Applied Mathematics, volume 653 of Lecture Notes in Computer Science, pages 129-153. Springer-Verlag, 1992.

• A. Pnueli. How Vital is Liveness? In W.R. Cleaveland, editor, Proceedings of Concur'92, volume 630 of Lecture Notes in Computer Science, pages 162-175. Springer-Verlag, 1992.

• O. Maler, Z. Manna, and A. Pnueli. From Timed to Hybrid Systems. In J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, editors, Proceedings of the REX Workshop ``Real-Time: Theory in Practice'', volume 600 of Lecture Notes in Computer Science, pages 447-484. Springer-Verlag, 1992.

• Y. Kesten, and A. Pnueli. Timed and Hybrid Statecharts and their Textual Representation. In J. Vytopil, editor, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 571 of Lecture Notes in Computer Science, pages 591-619. Springer-Verlag, 1992. [PostScript]
• T. Henzinger, Z. Manna, and A. Pnueli. What Good are Digital Clocks? In W. Kuich, editor, Proceedings of the 19th International Colloquium on Automata, Languages, and Programming (ICALP 1992), volume 623 of Lecture Notes in Computer Science, pages 545-558. Springer-Verlag, 1992.

• E.S. Chang, Z. Manna, and A. Pnueli. Characterization of Temporal Property Classes. In W. Kuich, editor, Proceedings of the 19th International Colloquium on Automata, Languages, and Programming (ICALP 1992), volume 623 of Lecture Notes in Computer Science, pages 474-486. Springer-Verlag, 1992.

• T. Henzinger, Z. Manna, and A. Pnueli. Timed Transition Systems. In J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, editors, Proceedings of the REX Workshop ``Real-Time: Theory in Practice'', volume 600 of Lecture Notes in Computer Science, pages 226-251. Springer-Verlag, 1992.

• Z. Manna, and A. Pnueli. Completing the Temporal Picture. Theoretical Computer Science, 83(1):97-130, 1991.

• Z. Manna, and A. Pnueli. Tools and Rules for the Practicing Verifier. In R. Rashid, editor, Carnegie Mellon Computer Science: A 25-year Commemorative, pages 121-156. ACM Press and Addison-Wesley, 1991.

• D. Peled, S. Katz, and A. Pnueli. Specifying and Proving Serializability in Temporal Logic. In Proceedings of the 6th IEEE Symposium Logic in Computer Science (LICS 1991), pages 232-244, 1991.

• O. Maler, and A. Pnueli. On the Learnability of Infinitary Regular Sets. In Proceedings of the 4th Annual Workshop on Computational Learning Theory, pages 128-136. Morgan Kaufmann Inc., 1991.

• Z. Manna, and A. Pnueli. On the Faithfulness of Formal Models. In Mathematical Foundation of Computer Science, volume 520 of Lecture Notes in Computer Science, pages 28-42. Springer-Verlag, 1991.

• A. Pnueli, and M. Shalev. What is in a Step: On the Semantics of Statecharts. In T. Ito and A. R. Meyer, editors, Theoretical Aspects of Computer Software, volume 526 of Lecture Notes in Computer Science, pages 244-264. Springer-Verlag, 1991.

• A. Kleinman, Y. Moscowitz, A. Pnueli, and E. Shapiro. Communication with Directed Logic Variables. In Proceedings of the 18th ACM Symposium Principles of Programming Languages (POPL 1991), 1991.

• T. Henzinger, Z. Manna, and A. Pnueli. Temporal Proof Methodologies for Real-Time Systems. In Proceedings of the 18th ACM Symposium Principles of Programming Languages (POPL 1991), pages 353-366, 1991.

• Z. Manna, and A. Pnueli. A Temporal Proof Methodology for Reactive Systems. In 5th Jerusalem Conference on Information Technology, pages 757-773, 1990.

• Z. Manna, and A. Pnueli. An Exercise in the Verification of Multi-Process Programs. In W.H.J. Feijen, A.J.M van Gasteren, D. Gries, and J. Misra, editors, Beauty is Our Business, pages 289-301. Springer-Verlag, 1990. (Gzipped PostScript, 15 pages, 51905 bytes)

• Z. Manna, and A. Pnueli. A Hierarchy of Temporal Properties. In Proceedings of the 9th ACM Symposium Principles of Distributed Computing (PODC 1990), pages 377-408, 1990.

• D. Harel, H. Lachover, A. Naamad, A. Pnueli, M. Politi, R. Sherman, A. Shtull-Trauring, and M. Trakhtenbrot. STATEMATE: A Working Environment for the Development of Complex Reactive Systems. IEEE Transactions Software Engineering, 16:403-414, 1990.

• T. Henzinger, Z. Manna, and A. Pnueli. An Interleaving Model for Real Time. In 5th Jerusalem Conference on Information Technology, pages 717-730, 1990.

• E. Harel, O. Lichtenstein, and A. Pnueli. Explicit Clock Temporal Logic. In Proceedings of the 5th IEEE Symposium Logic in Computer Science (LICS 1990), pages 402-413, 1990.

• O. Maler, and A. Pnueli. Tight Bounds on the Complexity of Cascaded Decomposition of Automata. In Proceedings of the 31th IEEE Symposium Foundations of Computer Science (FOCS 1990), pages 672-682, 1990.[Abstract]
• D. Peled, and A. Pnueli. Proving Partial Order Liveness Properties. In Proceedings of the 17th International Colloquium on Automata, Languages, and Programming (ICALP 1990), volume 443 of Lecture Notes in Computer Science, pages 553-571. Springer-Verlag, 1990.

• A. Pnueli, and R. Rosner. Distributed Reactive Systems are Hard to Synthesize. In Proceedings of the 31th IEEE Symposium Foundations of Computer Science (FOCS 1990), pages 746-757, 1990.

• Z. Manna, and A. Pnueli. The Anchored Version of the Temporal Framework. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, volume 354 of Lecture Notes in Computer Science, pages 201-284. Springer-Verlag, 1989. (Gzipped PostScript, 81 pages, 190020 bytes)

• A. Pnueli, and M. Shalev. What is in a Step? In J.W. Klop, J.-J.Ch. Meijer, and J.J.M.M. Rutten, editors, J.W. De Bakker, Liber Amicorum, pages 373-400. CWI, Amsterdam, 1989.

• A. Wilk, and A. Pnueli. Specification and Verification of VLSI Systems. In IEEE/ACM International Conference on Computer-Aided Design, pages 460-463, 1989.

• A. Pnueli, and R. Rosner. On the Synthesis of an Asynchronous Reactive Module. In Proceedings of the 16th International Colloquium on Automata, Languages, and Programming (ICALP 1989), volume 372 of Lecture Notes in Computer Science, pages 652-671. Springer-Verlag, 1989.

• Z. Manna, and A. Pnueli. Completing the Temporal Picture. In Proceedings of the 16th International Colloquium on Automata, Languages, and Programming (ICALP 1989), volume 372 of Lecture Notes in Computer Science, pages 534-558. Springer-Verlag, 1989.

• A. Pnueli, and R. Rosner. On the Synthesis of a Reactive Module. In Proceedings of the 16th ACM Symposium Principles of Programming Languages (POPL 1989), pages 179-190, 1989.

• A. Pnueli, and R. Rosner. A Framework for the Synthesis of Reactive Modules. In F.H. Vogt, editor, Proceeding of an International Conference on Concurrency: Concurrency 1988, volume 335 of Lecture Notes in Computer Science, pages 4-17. Springer-Verlag, 1988.

• A. Pnueli, and E. Harel. Applications of Temporal Logic to the Specification of Real Time Systems. In M. Joseph, editor, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 331 of Lecture Notes in Computer Science, pages 84-98. Springer-Verlag, 1988.

• S. Kaplan, and A. Pnueli. Specification and Implementation of Concurrently Accessed Data Structures: An Abstract Data Type Approach. In 4th Annual Symposium on Theoretical Aspects of Computer Science, volume 247 of Lecture Notes in Computer Science, pages 220-244. Springer-Verlag, 1987.

• Z. Manna, and A. Pnueli. Specification and Verification of Concurrent Programs by forall-Automata. In Proceedings of the 14th ACM Symposium Principles of Programming Languages (POPL 1987), pages 1-12, 1987.

• A. Pnueli. Specification and Development of Reactive Systems. In H.-J. Kugler, editor, Information Processing 86, pages 845-858. IFIP, North-Holland, 1986.

• A. Pnueli, and L. Zuck. Verification of Multiprocess Probabilistic Protocols. Distributed Computing, 1:53-72, 1986.

• R. Rosner, and A. Pnueli. A Choppy Logic. In Proceedings of the First IEEE Symposium Logic in Computer Science (LICS 1986), pages 306-313, 1986.

• A. Pnueli, and L. Zuck. Probablistic Verification by Tableaux. In Proceedings of the First IEEE Symposium Logic in Computer Science (LICS 1986), pages 322-331, 1986.

• A. Pnueli. Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Current Trends in Concurrency, volume 224 of Lecture Notes in Computer Science, pages 510-584. Springer-Verlag, 1986.

• D. Harel, A. Pnueli, J.P. Schmidt, and R. Sherman. On the Formal Semantics of Statecharts. In Proceedings of the 2nd IEEE Symposium Logic in Computer Science (LICS 1987), pages 54-64, 1987.

• H. Barringer, R. Kuiper, and A. Pnueli. A Really Abstract Concurrent Model and its Temporal Logic. In Proceedings of the 13th ACM Symposium Principles of Programming Languages (POPL 1986), pages 173-183, 1986.

• A. Pnueli. Linear and Branching Structures in the Semantics and Logics of Reactive Systems. In W. Brauer, editor, Proceedings of the 12th International Colloquium on Automata, Languages, and Programming (ICALP 1985), volume 194 of Lecture Notes in Computer Science, pages 15-32. Springer-Verlag, 1985.

• H. Barringer, R. Kuiper, and A. Pnueli. A Compositional Temporal Approach to a CSP-like Language. In E.J. Neuhold and G. Chroust, editors, Formal Models of Programming, pages 207-227. IFIP, North Holland, 1985.

• D. Harel, and A. Pnueli. On the Development of Reactive Systems. In K. R. Apt, editor, Logics and Models of Concurrent Systems, volume F-13 of NATO ASI Series, pages 477-498, New York, 1985. Springer-Verlag.

• A. Pnueli. In Transition from Global to Modular Temporal Reasoning about Programs. In K.R. Apt, editor, Logics and Models of Concurrent Systems, sub-series F: Computer and System Science, pages 123-144. Springer-Verlag, 1985.

• N. Francez, O. Grumberg, S. Katz, and A. Pnueli. Proving Termination of Prolog Programs. In Proc. Conf. Logics of Programs, volume 193 of Lecture Notes in Computer Science, pages 89-105. Springer-Verlag, 1985.

• O. Lichtenstein, A. Pnueli, and L. Zuck. The Glory of the Past. In Proceedings of the Conference on Logics of Programs, volume 193 of Lecture Notes in Computer Science, pages 196-218. Springer-Verlag, 1985.

• O. Lichtenstein, and A. Pnueli. Checking that Finite-State Concurrent Programs Satisfy their Linear Specification. In Proceedings of the 12th ACM Symposium Principles of Programming Languages (POPL 1985), pages 97-107, 1985.

• K.R. Apt, A. Pnueli, and J. Stavi. Fair Termination Revisited -- with Delay. Theoretical Computer Science, 33:65-84, 1984.

• R. Sherman, A. Pnueli, and D. Harel. Is the Interesting Part of Process Logic Uninteresting?: A Translation from PL to PDL. SIAM Journal Comp., 13:825-839, 1984.

• N. Francez, D. Lehmann, and A. Pnueli. A Linear History Semantics for Distributed Languages. Theoretical Computer Science, 32:25-46, 1984.

• S. Cohen, D. Lehmann, and A. Pnueli. Symmetric and Economical Solutions to the Mutual Exclusion Problem in a Distributed System. Theoretical Computer Science, 34:215-225, 1984.

• H. Barringer, R. Kuiper, and A. Pnueli. Now You May Compose Temporal Logic Specifications. In Proceedings of the 16th ACM Symposium Theory of Computing (STOC 1984), pages 51-63, 1984.

• M. Sharir, A. Pnueli, and S. Hart. Verification of Probabilistic Programs. SIAM Journal Comp., 13:292-314, 1984.

• Z. Manna, and A. Pnueli. Adequate Proof Principles for Invariance and Liveness Properties of Concurrent Programs. Science of Computer Programming, 32:257-289, 1984.

• D.E. Shasha, A. Pnueli, and E. Ewald. Temporal Verification of Carrier-Sense Local Area Network Protocols. In Proceedings of the 11th ACM Symposium Principles of Programming Languages (POPL 1984), pages 54-65, 1984.

• D. Ron, F. Rosemberg, and A. Pnueli. A Hardware Implementation of the CSP Primitives and its Verification. In Proceedings of the 11th International Colloquium on Automata, Languages, and Programming (ICALP 1984), volume 172 of Lecture Notes in Computer Science, pages 423-435. Springer-Verlag, 1984.

• D. Harel, A. Pnueli, and J. Stavi. Propositional Dynamic Logic of Non-Regular Programs. Journal of Computer and Systems Science, 26:222-243, 1983.

• N.S. Prywes, and A. Pnueli. Compilation of Non-Procedural Specifications into Computer Programs. IEEE Transactions Software Engineering, SE-9, 3:267-279, 1983.

• T. Koren, and A. Pnueli. There Exist Decidable Context-Free Propositional Dynamic Logics. In E.M. Clarke and D.C. Kozen, editors, Proc. Workshop on Logics of Programs, volume 164 of Lecture Notes in Computer Science, pages 290-312. Springer-Verlag, 1983.

• M. Ben-Ari, Z. Manna, and A. Pnueli. The Temporal Logic of Branching Time. Acta Informatica, 20:207-226, 1983.

• Z. Manna, and A. Pnueli. bf Verification of Concurrent Programs: A Temporal Proof System. In J.W. de Bakker and J. Van Leeuwen, editors, Foundations of Computer Science IV, Distributed Systems: Part 2, pages 163-255. Mathematical Centre Tracts 159, Center for Mathematics and Computer Science (CWI), Amsterdam, 1983.

• Z. Manna, and A. Pnueli. bf Proving Precedence Properties: The Temporal Way. In Proceedings of the 10th International Colloquium on Automata, Languages, and Programming (ICALP 1983), volume 154 of Lecture Notes in Computer Science, pages 491-512. Springer-Verlag, 1983.

• A. Pnueli. On the Extremely Fair Treatment of Probabilistic Algorithms. In Proceedings of the 15th ACM Symposium Theory of Computing (STOC 1983), pages 278-290, 1983.

• Z. Manna, and A. Pnueli. How to Cook a Temporal Proof System for Your Pet Language. In Proceedings of the 10th ACM Symposium Principles of Programming Languages (POPL 1983), pages 141-154, 1983.

• A. Pnueli, and W.P. deRoever. Rendez-vous with ADA - A Proof-Theoretical View. In Proceedings of the AdaTEC Conference on Ada, pages 129-137, Arlington, Va., 1982.

• S. Hart, M. Sharir, and A. Pnueli. Termination of Probabilistic Concurrent Programs. In Proceedings of the 9th ACM Symposium Principles of Programming Languages (POPL 1982), pages 1-6, 1982.

• A. Pnueli, and G. Slutzki. Automatic Programming of Finite-State Linear Programs. SIAM Journal Comp., 10:519-535, 1981.

• D. Harel, A. Pnueli, and J. Stavi. Propositional Dynamic Logic of Context-Free Programs. In Proceedings of the 22nd IEEE Symposium Foundations of Computer Science (FOCS 1981), pages 310-321, 1981.

• A. Pnueli. The Temporal Semantics of Concurrent Programs. Theoretical Computer Science, 13:1-20, 1981.

• A. Pnueli, and R. Zarhi. Realizing an Equational Specification. In Proceedings of the 8th International Colloquium on Automata, Languages, and Programming (ICALP 1981), volume 115 of Lecture Notes in Computer Science, pages 459-478. Springer-Verlag, 1981.

• Z. Manna, and A. Pnueli. Verification of Concurrent Programs: Temporal Proof Principles. In D.C. Kozen, editor, Proc. Workshop on Logics of Programs, volume 131 of Lecture Notes in Computer Science, pages 200-252. Springer-Verlag, 1981.

• Z. Manna, and A. Pnueli. bf Verification of Concurrent Programs: The Temporal Framework. In R.S. Boyer and J.S. Moore, editors, The Correctness Problem in Computer Science, pages 215-273. Academic Press, London, 1981.

• D. Lehmann, A. Pnueli, and J. Stavi. Impartiality, Justice and Fairness: The Ethics of Concurrent Termination. In Proceedings of the 8th International Colloquium on Automata, Languages, and Programming (ICALP 1981), volume 115 of Lecture Notes in Computer Science, pages 264-277. Springer-Verlag, 1981.

• M. Ben-Ari, J.Y. Halpern, and A. Pnueli. Deterministic Propositional Dynamic Logic: Finite Models, Complexity and Completeness. In Proceedings of the 8th International Colloquium on Automata, Languages, and Programming (ICALP 1981), volume 115 of Lecture Notes in Computer Science, pages 249-263. Springer-Verlag, 1981.

• M. Sharir, and A. Pnueli. Two Approaches to Inter-Procedural Data-Flow Analysis. In Jones and Muchnik, editors, Program Flow Analysis: Theory and Applications. Prentice-Hall, 1981.

• D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the Temporal Analysis of Fairness. In Proceedings of the 7th ACM Symposium Principles of Programming Languages (POPL 1980), pages 163-173, 1980.

• Z. Manna, and A. Pnueli. Synchronous Schemes and Their Decision Problems. In Proceedings of the 7th ACM Symposium Principles of Programming Languages (POPL 1980), pages 62-67, 1980.

• N.S. Prywes, A. Pnueli, and S. Shastry. Use of a Non-Procedural Specification Language and Associated Program Generator in Software Development. ACM Transactions on Programming Languages and Systems, 1:196-217, 1979.

• Z. Manna, and A. Pnueli. The Modal Logic of Programs. In Proceedings of the 6th International Colloquium on Automata, Languages, and Programming (ICALP 1979), volume 71 of Lecture Notes in Computer Science, pages 385-409. Springer-Verlag, 1979.

• A. Pnueli. The Temporal Semantics of Concurrent Programs. In G. Kahn, editor, Semantics of Concurrent Computations, volume 70 of Lecture Notes in Computer Science, pages 1-20. Springer-Verlag, 1979.

• N. Francez, and A. Pnueli. A Proof Method for Cyclic Programs. Acta Informatica, 9:133-157, 1978.

• A. Pnueli. The Temporal Logic of Programs. In Proceedings of the 18th IEEE Symposium Foundations of Computer Science (FOCS 1977), pages 46-57, 1977. (Gzipped PostScript)

• N. Francez, B. Klebanski, and A. Pnueli. Backtracking in Recursive Computation. Acta Informatica, 8:125-144, 1977.

• S. Shastry, A. Pnueli, and N.S. Prywes. Non-procedural Programming in Model. In IEEE Conference on Computer Software and Applications, pages 500-513, 1977.

• T. Olshansky, and A. Pnueli. A Direct Algorithm for Checking Equivalence of LL(k) Grammars. Theoretical Computer Science, 4:321-349, 1977.

• A. Pnueli, and G. Slutzki. Simple Programs and their Decision Problems. In Proceedings of the 4th International Colloquium on Automata, Languages, and Programming (ICALP 1977), 1977.

• D. Harel, A. Pnueli, and J. Stavi. A Complete Axiomatic System for Proving Deductions about Recursive Programs. In Proceedings of the 9th ACM Symposium Theory of Computing (STOC 1977), pages 249-260, 1977.

• N. Francez, and A. Pnueli. A Proof Method for Cyclic Concurrent and Sequential Programs. In Proceedings of the International Conference on Parallel Processing. Wayne State University, 1976.

• Z. Manna, and A. Pnueli. Axiomatic Approach to Total Correctness of Programs. Acta Informatica, 3:243-263, 1974.

• E. Ashcroft, Z. Manna, and A. Pnueli. Decidable Properties of Monadic Functional Schemes. Journal of the ACM, 20:489-499, 1973.

• S. Even, A. Lempel, and A. Pnueli. Permutation Graphs and Transitive Graphs. Journal of the ACM, 19:400-410, 1972.

• S. Even, A. Lempel, and A. Pnueli. Transitive Orientation of Undirected Graphs. Canadian Journal of Mathematics, 23:160-175, 1971.

• F. Commoner, A. Holt, S. Even, and A. Pnueli. Marked Directed Graphs. Journal of Computer and System Sciences, 5:511-523, 1971.

• A. Pnueli. An Improved Starting Point for Integer Linear Programming Algorithms. In B. Avi-Itzhak, editor, Developments in Operations Research. Gordon and Breach, London, 1971.

• Z. Manna, and A. Pnueli. Formalization of Properties of Functional Programs. Journal of the ACM, 17:555-569, 1970.

• A. Pnueli, and C.L. Pekeris. Free Tidal Oscillations in Rotating Flat Basins of the Form of Rectangles and of Sectors of Circles. Philosophical Transaction of the Royal Society, London, Series A, 263:149-171, 1968.

• A. Pnueli, and C.L. Pekeris. Tides in Oceans in the Form of a Cross. Proceedings of the Royal Society, Series A, 305:219-233, 1968.