Lenore D. Zuck

Lenore D. Zuck. Liveness to Safety for Distributed Systems. In On the Pursuit of Insight and Elegance - Essays Dedicated to Andreas Podelski on the Occasion of His 65th Birthday, Lecture Notes in Computer Science, pp. 23–39, Springer, 2026.

David A. Basin, Nate Foster, Kenneth L. McMillan, Kedar S. Namjoshi, Cristina Nita-Rotaru, Jonathan M. Smith, Pamela Zave, and Lenore D. Zuck. It Takes a Village: Bridging the Gaps between Current and Formal Specifications for Protocols. Commun. ACM, 68(8), 50–61, 2025.

Kedar S. Namjoshi and Lenore D. Zuck. Program Correctness through Self-Certification. Commun. ACM, 68(2), 74–84, 2025.

Lenore D. Zuck and Zhongkai Wen. Avoiding Spurious Timeouts. In Principles of Verification: Cycling the Probabilistic Landscape - Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part III, Lecture Notes in Computer Science, pp. 338–350, Springer, 2024.

Joel Miller, Rishi Advani, Ian A. Kash, Chris Kanich, and Lenore D. Zuck. Decentralized Fair Division. CoRR, abs/2408.07821, 2024.

Max von Hippel, Panagiotis Manolios, Kenneth L. McMillan, Cristina Nita-Rotaru, and Lenore D. Zuck. A Case Study in Analytic Protocol Analysis in ACL2. In Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, TX, USA and online, November 13-14, 2023, EPTCS, pp. 50–66, 2023.

Max von Hippel, Kenneth L. McMillan, Cristina Nita-Rotaru, and Lenore D. Zuck. A Formal Analysis of Karn's Algorithm. In Networked Systems - 11th International Conference, NETYS 2023, Benguerir, Morocco, May 22-24, 2023, Proceedings, Lecture Notes in Computer Science, pp. 43–61, Springer, 2023.

Ian A. Kash, Zhongkai Wen, and Lenore D. Zuck. Dynamic relocation in ridesharing via fixpoint construction. In Uncertainty in Artificial Intelligence, Proceedings of the Thirty-Eighth Conference on Uncertainty in Artificial Intelligence, UAI 2022, 1-5 August 2022, Eindhoven, The Netherlands, Proceedings of Machine Learning Research, pp. 980–989, PMLR, 2022.

Ufuk Topcu, Nadya Bliss, Nancy J. Cooke, Missy L. Cummings, Ashley J. Llorens, Howard E. Shrobe, and Lenore D. Zuck. Assured Autonomy: Path Toward Living With Autonomous Systems We Can Trust. CoRR, abs/2010.14443, 2020.

Kenneth L. McMillan and Lenore D. Zuck. Compositional Testing of Internet Protocols. In 2019 IEEE Cybersecurity Development, SecDev 2019, Tysons Corner, VA, USA, September 23-25, 2019, pp. 161–174, IEEE, 2019.

Kenneth L. McMillan and Lenore D. Zuck. Formal specification and testing of QUIC. In Proceedings of the ACM Special Interest Group on Data Communication, SIGCOMM 2019, Beijing, China, August 19-23, 2019, pp. 227–240, ACM, 2019.

Lenore D. Zuck and Kenneth L. McMillan. Invisible Invariants Are Neither. In From Reactive Systems to Cyber-Physical Systems - Essays Dedicated to Scott A. Smolka on the Occasion of His 65th Birthday, Lecture Notes in Computer Science, pp. 57–72, Springer, 2019.

Yiji Zhang and Lenore D. Zuck. Formal Verification of Optimizing Compilers. In Distributed Computing and Internet Technology - 14th International Conference, ICDCIT 2018, Bhubaneswar, India, January 11-13, 2018, Proceedings, Lecture Notes in Computer Science, pp. 50–65, Springer, 2018.

Lenore D. Zuck, Kenneth L. McMillan, and Jordan Torf. P^5 : Planner-less Proofs of Probabilistic Parameterized Protocols. In Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings, Lecture Notes in Computer Science, pp. 336–357, Springer, 2018.

Anna Bernasconi, Claudio Menghi, Paola Spoletini, Lenore D. Zuck, and Carlo Ghezzi. From Model Checking to a Temporal Proof for Partial Models. In Software Engineering and Formal Methods - 15th International Conference, SEFM 2017, Trento, Italy, September 4-8, 2017, Proceedings, Lecture Notes in Computer Science, pp. 54–69, Springer, 2017.

Anna Bernasconi, Claudio Menghi, Paola Spoletini, Lenore D. Zuck, and Carlo Ghezzi. From model checking to a temporal proof for partial models: preliminary example. CoRR, abs/1706.02701, 2017.

Rigel Gjomemo, Phu H. Phung, Edmund Ballou, Kedar S. Namjoshi, V. N. Venkatakrishnan, and Lenore D. Zuck. Leveraging Static Analysis Tools for Improving Usability of Memory Error Sanitization Compilers. In 2016 IEEE International Conference on Software Quality, Reliability and Security, QRS 2016, Vienna, Austria, August 1-3, 2016, pp. 323–334, IEEE, 2016.

Sanjiva Prasad and Lenore D. Zuck. Self-Similarity Breeds Resilience. In Proceedings Combined 23rd International Workshop on Expressiveness in Concurrency and 13th Workshop on Structural Operational Semantics, EXPRESS/SOS 2016, Québec City, Canada, 22nd August 2016, EPTCS, pp. 30–44, 2016.

Lenore D. Zuck and Sanjiva Prasad. A Switch, in Time. In Trustworthy Global Computing - 10th International Symposium, TGC 2015, Madrid, Spain, August 31 - September 1, 2015 Revised Selected Papers, Lecture Notes in Computer Science, pp. 131–146, Springer, 2015.

Rigel Gjomemo, Kedar S. Namjoshi, Phu H. Phung, V. N. Venkatakrishnan, and Lenore D. Zuck. From Verification to Optimizations. In Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings, Lecture Notes in Computer Science, pp. 300–317, Springer, 2015.

Lenore D. Zuck and Sanjiva Prasad. Limited Mobility, Eventual Stability. In Hardware and Software: Verification and Testing - 11th International Haifa Verification Conference, HVC 2015, Haifa, Israel, November 17-19, 2015, Proceedings, Lecture Notes in Computer Science, pp. 139–154, Springer, 2015.

Yliès Falcone and Lenore D. Zuck. Runtime verification: the application perspective. Int. J. Softw. Tools Technol. Transf., 17(2), 121–123, 2015.

Sven Dietrich, Jeroen van der Ham, Aiko Pras, Roland van Rijswijk-Deij, Darren Shou, Anna Sperotto, Aimee van Wynsberghe, and Lenore D. Zuck. Ethics in Data Sharing: Developing a Model for Best Practice. In 35. IEEE Security and Privacy Workshops, SPW 2014, San Jose, CA, USA, May 17-18, 2014, pp. 5–9, IEEE Computer Society, 2014.

Timothy L. Hinrichs, A. Prasad Sistla, and Lenore D. Zuck. Model Check What You Can, Runtime Verify the Rest. In HOWARD-60: A Festschrift on the Occasion of Howard Barringer's 60th Birthday, pp. 234–244, EasyChair, 2014.

Lenore D. Zuck and Kenneth L. McMillan. Reasoning about Network Topologies in Space. In From Programs to Systems. The Systems perspective in Computing - ETAPS Workshop, FPS 2014, in Honor of Joseph Sifakis, Grenoble, France, April 6, 2014. Proceedings, Lecture Notes in Computer Science, pp. 267–277, Springer, 2014.

Kedar S. Namjoshi, Giacomo Tagliabue, and Lenore D. Zuck. A Witnessing Compiler: A Proof of Concept. In Runtime Verification - 4th International Conference, RV 2013, Rennes, France, September 24-27, 2013. Proceedings, Lecture Notes in Computer Science, pp. 340–345, Springer, 2013.

Timothy L. Hinrichs, Diego Martinoia, William C. Garrison III, Adam J. Lee, Alessandro Panebianco, and Lenore D. Zuck. Application-Sensitive Access Control Evaluation Using Parameterized Expressiveness. In 2013 IEEE 26th Computer Security Foundations Symposium, New Orleans, LA, USA, June 26-28, 2013, pp. 145–160, IEEE Computer Society, 2013.

Nazari Skrupsky, Prithvi Bisht, Timothy L. Hinrichs, V. N. Venkatakrishnan, and Lenore D. Zuck. TamperProof: a server-agnostic defense for parameter tampering attacks on web applications. In Third ACM Conference on Data and Application Security and Privacy, CODASPY'13, San Antonio, TX, USA, February 18-20, 2013, pp. 129–140, ACM, 2013.

Timothy L. Hinrichs, Daniele Rossetti, Gabriele Petronella, V. N. Venkatakrishnan, A. Prasad Sistla, and Lenore D. Zuck. WEBLOG: a declarative language for secure web development. In Proceedings of the 2013 ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, PLAS 2013, Seattle, WA, USA, June 20, 2013, pp. 59–70, ACM, 2013.

Kedar S. Namjoshi and Lenore D. Zuck. Witnessing Program Transformations. In Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings, Lecture Notes in Computer Science, pp. 304–323, Springer, 2013.

Nazari Skrupsky, Maliheh Monshizadeh, Prithvi Bisht, Timothy L. Hinrichs, Venkat N. Venkatakrishnan, and Lenore D. Zuck. Don't Repeat Yourself: Automatically Synthesizing Client-side Validation Code for Web Applications. In 3rd USENIX Conference on Web Application Development, WebApps'12, Boston, MA, USA, June 13, 2012, pp. 107–108, USENIX Association, 2012.

Ahmed Bouajjani, David Harel, and Lenore D. Zuck. Editor's foreword. J. Comput. Syst. Sci., 78(3), 822, 2012.

José M. Fernandez, Andrew S. Patrick, and Lenore D. Zuck. Ethical and Secure Data Sharing across Borders. In Financial Cryptography and Data Security - FC 2012 Workshops, USEC and WECSR 2012, Kralendijk, Bonaire, March 2, 2012, Revised Selected Papers, Lecture Notes in Computer Science, pp. 136–140, Springer, 2012.

Matthew L. Bolton, Celeste M. Wallace, and Lenore D. Zuck. On Policies and Intents. In Information Systems Security, 8th International Conference, ICISS 2012, Guwahati, India, December 15-19, 2012. Proceedings, Lecture Notes in Computer Science, pp. 104–118, Springer, 2012.

Yliès Falcone and Lenore D. Zuck. Runtime Verification: The Application Perspective. In Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change - 5th International Symposium, ISoLA 2012, Heraklion, Crete, Greece, October 15-18, 2012, Proceedings, Part I, Lecture Notes in Computer Science, pp. 284–291, Springer, 2012.

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

Nazari Skrupsky, Maliheh Monshizadeh, Prithvi Bisht, Timothy L. Hinrichs, V. N. Venkatakrishnan, and Lenore D. Zuck. WAVES: Automatic Synthesis of Client-Side Validation Code for Web Applications. In 2012 ASE International Conference on Cyber Security, Alexandria, VA, USA, December 14-16, 2012, pp. 46–53, IEEE Computer Society, 2012.

Kenneth L. McMillan and Lenore D. Zuck. Invisible Invariants and Abstract Interpretation. In Static Analysis - 18th International Symposium, SAS 2011, Venice, Italy, September 14-16, 2011. Proceedings, Lecture Notes in Computer Science, pp. 249–262, Springer, 2011.

Amir Pnueli, Yaniv Sa'ar, and Lenore D. Zuck. Jtlv: A Framework for Developing Verification Algorithms. In Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, Lecture Notes in Computer Science, pp. 171–174, Springer, 2010.

Ariel Cohen, Kedar S. Namjoshi, Yaniv Sa'ar, Lenore D. Zuck, and Katya I. Kisyova. Parallelizing a Symbolic Compositional Model-Checking Algorithm. In Hardware and Software: Verification and Testing - 6th International Haifa Verification Conference, HVC 2010, Haifa, Israel, October 4-7, 2010. Revised Selected Papers, Lecture Notes in Computer Science, pp. 46–59, Springer, 2010.

Ittai Balaban, Amir Pnueli, and Lenore D. Zuck. Proving the Refuted: Symbolic Model Checkers as Proof Generators. In Concurrency, Compositionality, and Correctness, Essays in Honor of Willem-Paul de Roever, Lecture Notes in Computer Science, pp. 221–236, Springer, 2010.

Kenneth L. McMillan and Lenore D. Zuck. Abstract Counterexamples for Non-disjunctive Abstractions. In Reachability Problems, 3rd International Workshop, RP 2009, Palaiseau, France, September 23-25, 2009. Proceedings, Lecture Notes in Computer Science, pp. 176–188, Springer, 2009.

Ariel Cohen, Ron van der Meyden, and Lenore D. Zuck. Access Control and Information Flow in Transactional Memory. In Formal Aspects in Security and Trust, 5th International Workshop, FAST 2008, Malaga, Spain, October 9-10, 2008, Revised Selected Papers, Lecture Notes in Computer Science, pp. 316–330, Springer, 2008.

Ariel Cohen, Amir Pnueli, and Lenore D. Zuck. Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses. In Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings, Lecture Notes in Computer Science, pp. 121–134, Springer, 2008.

Venkatram Vishwanath, Lenore D. Zuck, and Jason Leigh. Specification and Verification of LambdaRAM: A Wide-area Distributed Cache for High Performance Computing. In 6th ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2008), June 5-7, 2008, Anaheim, CA, USA, pp. 187–198, IEEE Computer Society, 2008.

Verification, Model Checking, and Abstract Interpretation, 9th International Conference, VMCAI 2008, San Francisco, USA, January 7-9, 2008, Proceedings. Lecture Notes in Computer Science, Springer, 2008.

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

Ittai Balaban, Amir Pnueli, and Lenore D. Zuck. Shape Analysis of Single-Parent Heaps. In Verification, Model Checking, and Abstract Interpretation, 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings, Lecture Notes in Computer Science, pp. 91–105, Springer, 2007.

Saddek Bensalem, Doron A. Peled, Hongyang Qu, Stavros Tripakis, and Lenore D. Zuck. Test Case Generation for Ultimately Periodic Paths. In Hardware and Software: Verification and Testing, Third International Haifa Verification Conference, HVC 2007, Haifa, Israel, October 23-25, 2007, Proceedings, Lecture Notes in Computer Science, pp. 120–135, Springer, 2007.

Ariel Cohen, John W. O'Leary, Amir Pnueli, Mark R. Tuttle, and Lenore D. Zuck. Verifying Correctness of Transactional Memories. In Formal Methods in Computer-Aided Design, 7th International Conference, FMCAD 2007, Austin, Texas, USA, November 11-14, 2007, Proceedings, pp. 37–44, IEEE Computer Society, 2007.

Yi Fang and Lenore D. Zuck. Improved Invariant Generation for Tvoc. In Proceedings of the 5th International Workshop on Compiler Optimization meets Compiler Verification, COCV@ETAPS 2006, Vienna, Austria, April 2, 2006, Electronic Notes in Theoretical Computer Science, pp. 21–35, Elsevier, 2006.

Ittai Balaban, Amir Pnueli, and Lenore D. Zuck. Invisible Safety of Distributed Protocols. In Automata, Languages and Programming, 33rd International Colloquium, ICALP 2006, Venice, Italy, July 10-14, 2006, Proceedings, Part II, Lecture Notes in Computer Science, pp. 528–539, Springer, 2006.

Yi Fang, Kenneth L. McMillan, Amir Pnueli, and Lenore D. Zuck. Liveness by Invisible Invariants. In Formal Techniques for Networked and Distributed Systems - FORTE 2006, 26th IFIP WG 6.1 International Conference, Paris, France, September 26-29, 2006, Lecture Notes in Computer Science, pp. 356–371, Springer, 2006.

Yi Fang, Nir Piterman, Amir Pnueli, and Lenore D. Zuck. Liveness with invisible ranking. Int. J. Softw. Tools Technol. Transf., 8(3), 261–279, 2006.

A. Prasad Sistla, Min Zhou, and Lenore D. Zuck. Monitoring Off-the-Shelf Components. In Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings, Lecture Notes in Computer Science, pp. 222–236, Springer, 2006.

Tamarah Arons, Elad Elster, Limor Fix, Sela Mador-Haim, Michael Mishaeli, Jonathan Shalev, Eli Singerman, Andreas Tiemeyer, Moshe Y. Vardi, and Lenore D. Zuck. Formal Verification of Backward Compatibility of Microcode. In Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings, Lecture Notes in Computer Science, pp. 185–198, Springer, 2005.

Cory Plock, Benjamin Goldberg, and Lenore D. Zuck. From Requirements to Specifications. In 12th IEEE International Conference on the Engineering of Computer-Based Systems (ECBS 2005), 4-7 April 2005, Greenbelt, MD, USA, pp. 183–190, IEEE Computer Society, 2005.

Ittai Balaban, Yi Fang, Amir Pnueli, and Lenore D. Zuck. IIV: An Invisible Invariant Verifier. In Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings, Lecture Notes in Computer Science, pp. 408–412, Springer, 2005.

Amir Pnueli, Aleksandr Zaks, and Lenore D. Zuck. Monitoring Interfaces for Faults. In Proceedings of the Fifth Workshop on Runtime Verification, RV@CAV 2005, Edinburgh, UK, July 12, 2005, Electronic Notes in Theoretical Computer Science, pp. 73–89, Elsevier, 2005.

Ittai Balaban, Amir Pnueli, and Lenore D. Zuck. Ranking Abstraction as Companion to Predicate Abstraction. In Formal Techniques for Networked and Distributed Systems - FORTE 2005, 25th IFIP WG 6.1 International Conference, Taipei, Taiwan, October 2-5, 2005, Proceedings, Lecture Notes in Computer Science, pp. 1–12, Springer, 2005.

Ittai Balaban, Amir Pnueli, and Lenore D. Zuck. Shape Analysis by Predicate Abstraction. In Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings, Lecture Notes in Computer Science, pp. 164–180, Springer, 2005.

Tiziana Margaria, A. Prasad Sistla, Bernhard Steffen, and Lenore D. Zuck. Taming Interface Specifications. In CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings, Lecture Notes in Computer Science, pp. 548–561, Springer, 2005.

Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings. Lecture Notes in Computer Science, Springer, 2005.

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

Clark W. Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, and Lenore D. Zuck. TVOC: A Translation Validator for Optimizing Compilers. In Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings, Lecture Notes in Computer Science, pp. 291–295, Springer, 2005.

Benjamin Goldberg, Lenore D. Zuck, and Clark W. Barrett. Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers. In Proceedings of the 3rd International Workshop on Compiler Optimization Meets Compiler Verification, COCV@ETAPS 2004, Barcelona, Spain, April 3, 2004, Electronic Notes in Theoretical Computer Science, pp. 53–71, Elsevier, 2004.

Yi Fang, Nir Piterman, Amir Pnueli, and Lenore D. Zuck. Liveness with Incomprehensible Ranking. In Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings, Lecture Notes in Computer Science, pp. 482–496, Springer, 2004.

Yi Fang, Nir Piterman, Amir Pnueli, and Lenore D. Zuck. Liveness with Invisible Ranking. In Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, Italy, January 11-13, 2004, Proceedings, Lecture Notes in Computer Science, pp. 223–238, Springer, 2004.

Lenore D. Zuck and Amir Pnueli. Model checking and abstraction to the aid of parameterized systems (a survey). Comput. Lang. Syst. Struct., 30(3-4), 139–169, 2004.

Lenore D. Zuck, Paul C. Attie, and Agostino Cortesi. Preface by the section editors. Int. J. Softw. Tools Technol. Transf., 6(1), 1–3, 2004.

Lenore D. Zuck. Special issue of VMCAI'03. Comput. Lang. Syst. Struct., 30(3-4), 97–98, 2004.

Joshua D. Guttman, F. Javier Thayer, and Lenore D. Zuck. The faithfulness of abstract protocol analysis: Message authentication. J. Comput. Secur., 12(6), 865–891, 2004.

Amir Pnueli and Lenore D. Zuck. Model-Checking and Abstraction to the Aid of Parameterized Systems. In Verification, Model Checking, and Abstract Interpretation, 4th International Conference, VMCAI 2003, New York, NY, USA, January 9-11, 2002, Proceedings, Lecture Notes in Computer Science, pp. 4, Springer, 2003.

Tamarah Arons, Amir Pnueli, and Lenore D. Zuck. Parameterized Verification by Probabilistic Abstraction. In Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, Lecture Notes in Computer Science, pp. 87–102, Springer, 2003.

Clark W. Barrett, Benjamin Goldberg, and Lenore D. Zuck. Run-Time Validation of Speculative Optimizations using CVC. In Third Workshop on Run-time Verification, RV@CAV 2003, Boulder, Colorado, USA, July 14, 2003, Electronic Notes in Theoretical Computer Science, pp. 89–107, Elsevier, 2003.

Verification, Model Checking, and Abstract Interpretation, 4th International Conference, VMCAI 2003, New York, NY, USA, January 9-11, 2002, Proceedings. Lecture Notes in Computer Science, Springer, 2003.

Lenore D. Zuck, Amir Pnueli, and Benjamin Goldberg. VOC: A Methodology for the Translation Validation of OptimizingCompilers. J. Univers. Comput. Sci., 9(3), 223–247, 2003.

Lenore D. Zuck, Amir Pnueli, and Yonit Kesten. Automatic Verification of Probabilistic Free Choice. In Verification, Model Checking, and Abstract Interpretation, Third International Workshop, VMCAI 2002, Venice, Italy, January 21-22, 2002, Revised Papers, Lecture Notes in Computer Science, pp. 208–224, Springer, 2002.

Amir Pnueli, Jessie Xu, and Lenore D. Zuck. Liveness with (0, 1, infty)-Counter Abstraction. In Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings, Lecture Notes in Computer Science, pp. 107–122, Springer, 2002.

Yonit Kesten, Amir Pnueli, Elad Shahar, and Lenore D. Zuck. Network Invariants in Action. In CONCUR 2002 - Concurrency Theory, 13th International Conference, Brno, Czech Republic, August 20-23, 2002, Proceedings, Lecture Notes in Computer Science, pp. 101–115, Springer, 2002.

Lenore D. Zuck, Amir Pnueli, Yi Fang, Benjamin Goldberg, and Ying Hu. Translation and Run-Time Validation of Optimized Code. In Runtime Verification 2002, RV 2002, FLoC Satellite Event, Copenhagen, Denmark, July 26, 2002, Electronic Notes in Theoretical Computer Science, pp. 179–200, Elsevier, 2002.

Lenore D. Zuck, Amir Pnueli, Yi Fang, and Benjamin Goldberg. VOC: A Translation Validator for Optimizing Compilers. In Compiler Optimization Meets Compiler Verification, COCV 2002, Satellite Event of ETAPS 2002, Grenoble, France, April 13, 2002, Electronic Notes in Theoretical Computer Science, pp. 2–18, Elsevier, 2002.

Amir Pnueli, Sitvanit Ruah, and Lenore D. Zuck. Automatic Deductive Verification with Invisible Invariants. In Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings, Lecture Notes in Computer Science, pp. 82–97, Springer, 2001.

Doron A. Peled, Amir Pnueli, and Lenore D. Zuck. From Falsification to Verification. In FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science, 21st Conference, Bangalore, India, December 13-15, 2001, Proceedings, Lecture Notes in Computer Science, pp. 292–304, Springer, 2001.

Doron A. Peled and Lenore D. Zuck. From Model Checking to a Temporal Proof. In Model Checking Software, 8th International SPIN Workshop, Toronto, Canada, May 19-20, 2001, Proceedings, Lecture Notes in Computer Science, pp. 1–14, Springer, 2001.

Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Jiazhao Xu, and Lenore D. Zuck. Parameterized Verification with Automatically Computed Inductive Assertions. In Computer Aided Verification, 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001, Proceedings, Lecture Notes in Computer Science, pp. 221–234, Springer, 2001.

Joshua D. Guttman, F. Javier Thayer, and Lenore D. Zuck. The faithfulness of abstract protocol analysis: message authentication. In CCS 2001, Proceedings of the 8th ACM Conference on Computer and Communications Security, Philadelphia, Pennsylvania, USA, November 6-8, 2001, pp. 186–195, ACM, 2001.

David Gelernter and Lenore D. Zuck. On What Linda Is: Formal Description of Linda as a Reactive System. In Coordination Languages and Models, Second International Conference, COORDINATION '97, Berlin, Germany, September 1-3, 1997, Proceedings, Lecture Notes in Computer Science, pp. 187–204, Springer, 1997.

Jeffery R. Westbrook and Lenore D. Zuck. Adaptive Algorithms for PASO Systems. In Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed Computing, Los Angeles, California, USA, August 14-17, 1994, pp. 264–273, ACM, 1994.

Nicholas Carriero, David Gelernter, and Lenore D. Zuck. Bauhaus Linda. In Object-Based Models and Languages for Concurrent Systems, ECOOP'94 Workshop on Models and Languages for Coordination of Parallelism and Distribution, Bologna, Italy, July 5, 1994, Selected Papers, Lecture Notes in Computer Science, pp. 66–76, Springer, 1994.

Yehuda Afek, Hagit Attiya, Alan D. Fekete, Michael J. Fischer, Nancy A. Lynch, Yishay Mansour, Da-Wei Wang, and Lenore D. Zuck. Reliable Communication Over Unreliable Channels. J. ACM, 41(6), 1267–1297, 1994.

Amir Pnueli and Lenore D. Zuck. In and Out of Temporal Logic. In Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS '93), Montreal, Canada, June 19-23, 1993, pp. 124–135, IEEE Computer Society, 1993.

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

A. Prasad Sistla and Lenore D. Zuck. Reasoning in a Restricted Temporal Logic. Inf. Comput., 102(2), 167–195, 1993.

Joseph Y. Halpern and Lenore D. Zuck. A Little Knowledge Goes a Long Way: Knowledge-Based Derivations and Correctness Proofs for a Family of Protocols. J. ACM, 39(3), 449–478, 1992.

Nick Reingold, Da-Wei Wang, and Lenore D. Zuck. Games I/O Automata Play (Extended Abstract). In CONCUR '92, Third International Conference on Concurrency Theory, Stony Brook, NY, USA, August 24-27, 1992, Proceedings, Lecture Notes in Computer Science, pp. 325–339, Springer, 1992.

Henri B. Weinberg and Lenore D. Zuck. Timed Ethernet: Real-Time Formal Specification of Ethernet. In CONCUR '92, Third International Conference on Concurrency Theory, Stony Brook, NY, USA, August 24-27, 1992, Proceedings, Lecture Notes in Computer Science, pp. 370–385, Springer, 1992.

A. Prasad Sistla and Lenore D. Zuck. Automatic Temporal Verification of Buffer Systems. In Computer Aided Verification, 3rd International Workshop, CAV '91, Aalborg, Denmark, July, 1-4, 1991, Proceedings, Lecture Notes in Computer Science, pp. 59–69, Springer, 1991.

Da-Wei Wang and Lenore D. Zuck. Real-Time Sequence Transmission Problem. In Proceedings of the Tenth Annual ACM Symposium on Principles of Distributed Computing, Montreal, Quebec, Canada, August 19-21, 1991, pp. 111–123, ACM, 1991.

Da-Wei Wang and Lenore D. Zuck. Tight Bounds for the Sequence Transmission Problem. In Proceedings of the Eighth Annual ACM Symposium on Principles of Distributed Computing, Edmonton, Alberta, Canada, August 14-16, 1989, pp. 73–83, ACM, 1989.

Michael J. Fischer and Lenore D. Zuck. Reasoning about Uncertainty in Fault-tolerant Distributed Systems. In Formal Techniques in Real-Time and Fault-Tolerant Systems, Proceedings of a Symposium, Warwick, UK, September 22-23, 1988, Lecture Notes in Computer Science, pp. 142–158, Springer, 1988.

A. Prasad Sistla and Lenore D. Zuck. On the Eventuality Operator in Temporal Logic. In Proceedings of the Symposium on Logic in Computer Science (LICS '87), Ithaca, New York, USA, June 22-25, 1987, pp. 153–166, IEEE Computer Society, 1987.

Amir Pnueli and Lenore D. Zuck. Probabilistic Verification by Tableaux. In Proceedings of the Symposium on Logic in Computer Science (LICS '86), Cambridge, Massachusetts, USA, June 16-18, 1986, pp. 322–331, IEEE Computer Society, 1986.

Amir Pnueli and Lenore D. Zuck. Verification of Multiprocess Probabilistic Protocols. Distributed Comput., 1(1), 53–72, 1986.

Orna Lichtenstein, Amir Pnueli, and Lenore D. Zuck. The Glory of the Past. In Logics of Programs, Conference, Brooklyn College, New York, NY, USA, June 17-19, 1985, Proceedings, Lecture Notes in Computer Science, pp. 196–218, Springer, 1985.

Amir Pnueli and Lenore D. Zuck. Verification of Multiprocess Probabilistic Protocols. In Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing, Vancouver, B. C., Canada, August 27-29, 1984, pp. 12–27, ACM, 1984.