The Glory of the Past. - Orna Lichtenstein; Amir Pnueli; Lenore D. Zuck (Logic of Programs, 1985)

Probabilistic Verification by Tableaux - Amir Pnueli; Lenore D. Zuck (LICS, 1986)

Verification of Multiprocess Probabilistic Protocols. - Amir Pnueli; Lenore D. Zuck (Distributed Comput., 1986)

On the Eventuality Operator in Temporal Logic - A. Prasad Sistla; Lenore D. Zuck (LICS, 1987)

Reasoning about Uncertainty in Fault-tolerant Distributed Systems. - Michael J. Fischer; Lenore D. Zuck (FTRTFT, 1988)

Tight Bounds for the Sequence Transmission Problem. - Da-Wei Wang; Lenore D. Zuck (PODC, 1989)

Automatic Temporal Verification of Buffer Systems. - A. Prasad Sistla; Lenore D. Zuck (CAV, 1991)

Real-Time Sequence Transmission Problem. - Da-Wei Wang; Lenore D. Zuck (PODC, 1991)

Games I/O Automata Play (Extended Abstract). - Nick Reingold; Da-Wei Wang; Lenore D. Zuck (CONCUR, 1992)

Timed Ethernet: Real-Time Formal Specification of Ethernet. - Henri B. Weinberg; Lenore D. Zuck (CONCUR, 1992)

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

In and Out of Temporal Logic - Amir Pnueli; Lenore D. Zuck (LICS, 1993)

Reasoning in a Restricted Temporal Logic - A. Prasad Sistla; Lenore D. Zuck (Inf. Comput., 1993)

Probabilistic Verification - Amir Pnueli; Lenore D. Zuck (Inf. Comput., 1993)

Bauhaus Linda. - Nicholas Carriero; David Gelernter; Lenore D. Zuck (ECOOP Workshop, 1994)

Adaptive Algorithms for PASO Systems. - Jeffery R. Westbrook; Lenore D. Zuck (PODC, 1994)

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

On What Linda Is: Formal Description of Linda as a Reactive System. - David Gelernter; Lenore D. Zuck (COORDINATION, 1997)

Parameterized Verification with Automatically Computed Inductive Assertions. - Tamarah Arons; Amir Pnueli; Sitvanit Ruah; Jiazhao Xu; Lenore D. Zuck (CAV, 2001)

From Falsification to Verification. - Doron A. Peled; Amir Pnueli; Lenore D. Zuck (FSTTCS, 2001)

From Model Checking to a Temporal Proof. - Doron A. Peled; Lenore D. Zuck (SPIN, 2001)

Automatic Deductive Verification with Invisible Invariants. - Amir Pnueli; Sitvanit Ruah; Lenore D. Zuck (TACAS, 2001)

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

Network Invariants in Action. - Yonit Kesten; Amir Pnueli; Elad Shahar; Lenore D. Zuck (CONCUR, 2002)

Automatic Verification of Probabilistic Free Choice. - Lenore D. Zuck; Amir Pnueli; Yonit Kesten (VMCAI, 2002)

VOC: A Translation Validator for Optimizing Compilers. - Lenore D. Zuck; Amir Pnueli; Yi Fang 001; Benjamin Goldberg 001 (COCV@ETAPS, 2002)

Translation and Run-Time Validation of Optimized Code. - Lenore D. Zuck; Amir Pnueli; Yi Fang 001; Benjamin Goldberg 001; Ying Hu 003 (RV@FLoC, 2002)

Parameterized Verification by Probabilistic Abstraction. - Tamarah Arons; Amir Pnueli; Lenore D. Zuck (FoSSaCS, 2003)

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

Run-Time Validation of Speculative Optimizations using CVC. - Clark W. Barrett; Benjamin Goldberg 001; Lenore D. Zuck (RV@CAV, 2003)

VOC: A Methodology for the Translation Validation of OptimizingCompilers. - Lenore D. Zuck; Amir Pnueli; Benjamin Goldberg 001 (J. Univers. Comput. Sci., 2003)

Liveness with Incomprehensible Ranking. - Yi Fang 001; Nir Piterman; Amir Pnueli; Lenore D. Zuck (TACAS, 2004)

Special issue of VMCAI'03. - Lenore D. Zuck (Comput. Lang. Syst. Struct., 2004)

Model checking and abstraction to the aid of parameterized systems (a survey). - Lenore D. Zuck; Amir Pnueli (Comput. Lang. Syst. Struct., 2004)

Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers. - Benjamin Goldberg 001; Lenore D. Zuck; Clark W. Barrett (COCV@ETAPS, 2004)

The faithfulness of abstract protocol analysis: Message authentication. - Joshua D. Guttman; F. Javier Thayer; Lenore D. Zuck (J. Comput. Secur., 2004)

Preface by the section editors. - Lenore D. Zuck; Paul C. Attie; Agostino Cortesi (Int. J. Softw. Tools Technol. Transf., 2004)

Formal Verification of Backward Compatibility of Microcode. - Tamarah Arons; Elad Elster; Limor Fix; Sela Mador-Haim; Michael Mishaeli; Jonathan Shalev; Eli Singerman; Andreas Tiemeyer; Moshe Y. Vardi; Lenore D. Zuck (CAV, 2005)

IIV: An Invisible Invariant Verifier. - Ittai Balaban; Yi Fang 001; Amir Pnueli; Lenore D. Zuck (CAV, 2005)

TVOC: A Translation Validator for Optimizing Compilers. - Clark W. Barrett; Yi Fang 001; Benjamin Goldberg 001; Ying Hu 003; Amir Pnueli; Lenore D. Zuck (CAV, 2005)

Taming Interface Specifications. - Tiziana Margaria; A. Prasad Sistla; Bernhard Steffen; Lenore D. Zuck (CONCUR, 2005)

From Requirements to Specifications. - Cory Plock; Benjamin Goldberg 001; Lenore D. Zuck (ECBS, 2005)

Ranking Abstraction as Companion to Predicate Abstraction. - Ittai Balaban; Amir Pnueli; Lenore D. Zuck (FORTE, 2005)

Shape Analysis by Predicate Abstraction. - Ittai Balaban; Amir Pnueli; Lenore D. Zuck (VMCAI, 2005)

Monitoring Interfaces for Faults. - Amir Pnueli; Aleksandr Zaks; Lenore D. Zuck (RV@CAV, 2005)

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

Liveness by Invisible Invariants. - Yi Fang 001; Kenneth L. McMillan; Amir Pnueli; Lenore D. Zuck (FORTE, 2006)

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

Monitoring Off-the-Shelf Components. - A. Prasad Sistla; Min Zhou; Lenore D. Zuck (VMCAI, 2006)

Improved Invariant Generation for Tvoc. - Yi Fang 001; Lenore D. Zuck (COCV@ETAPS, 2006)

Liveness with invisible ranking. - Yi Fang 001; Nir Piterman; Amir Pnueli; Lenore D. Zuck (Int. J. Softw. Tools Technol. Transf., 2006)

Verifying Correctness of Transactional Memories. - Ariel Cohen 002; John W. O'Leary; Amir Pnueli; Mark R. Tuttle; Lenore D. Zuck (FMCAD, 2007)

Test Case Generation for Ultimately Periodic Paths. - Saddek Bensalem; Doron A. Peled; Hongyang Qu 001; Stavros Tripakis; Lenore D. Zuck (Haifa Verification Conference, 2007)

Shape Analysis of Single-Parent Heaps. - Ittai Balaban; Amir Pnueli; Lenore D. Zuck (VMCAI, 2007)

Modular Ranking Abstraction. - Ittai Balaban; Amir Pnueli; Lenore D. Zuck (Int. J. Found. Comput. Sci., 2007)

Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses. - Ariel Cohen 002; Amir Pnueli; Lenore D. Zuck (CAV, 2008)

Access Control and Information Flow in Transactional Memory. - Ariel Cohen 002; Ron van der Meyden; Lenore D. Zuck (Formal Aspects in Security and Trust, 2008)

Specification and Verification of LambdaRAM: A Wide-area Distributed Cache for High Performance Computing. - Venkatram Vishwanath; Lenore D. Zuck; Jason Leigh (MEMOCODE, 2008)

Abstract Counterexamples for Non-disjunctive Abstractions. - Kenneth L. McMillan; Lenore D. Zuck (RP, 2009)

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

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

Parallelizing a Symbolic Compositional Model-Checking Algorithm. - Ariel Cohen 002; Kedar S. Namjoshi; Yaniv Sa'ar; Lenore D. Zuck; Katya I. Kisyova (Haifa Verification Conference, 2010)

Invisible Invariants and Abstract Interpretation. - Kenneth L. McMillan; Lenore D. Zuck (SAS, 2011)

WAVES: Automatic Synthesis of Client-Side Validation Code for Web Applications. - Nazari Skrupsky; Maliheh Monshizadeh; Prithvi Bisht; Timothy L. Hinrichs; V. N. Venkatakrishnan; Lenore D. Zuck (CyberSecurity, 2012)

Ethical and Secure Data Sharing across Borders. - José M. Fernandez 001; Andrew S. Patrick; Lenore D. Zuck (Financial Cryptography Workshops, 2012)

On Policies and Intents. - Matthew L. Bolton; Celeste M. Wallace; Lenore D. Zuck (ICISS, 2012)

Don't Repeat Yourself: Automatically Synthesizing Client-side Validation Code for Web Applications. - Nazari Skrupsky; Maliheh Monshizadeh; Prithvi Bisht; Timothy L. Hinrichs; Venkat N. Venkatakrishnan; Lenore D. Zuck (WebApps, 2012)

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

Editorʼs foreword. - Ahmed Bouajjani; David Harel; Lenore D. Zuck (J. Comput. Syst. Sci., 2012)

TamperProof: a server-agnostic defense for parameter tampering attacks on web applications. - Nazari Skrupsky; Prithvi Bisht; Timothy L. Hinrichs; V. N. Venkatakrishnan; Lenore D. Zuck (CODASPY, 2013)

Application-Sensitive Access Control Evaluation Using Parameterized Expressiveness. - Timothy L. Hinrichs; Diego Martinoia; William C. Garrison III; Adam J. Lee; Alessandro Panebianco; Lenore D. Zuck (CSF, 2013)

WEBLOG: a declarative language for secure web development. - Timothy L. Hinrichs; Daniele Rossetti; Gabriele Petronella; V. N. Venkatakrishnan; A. Prasad Sistla; Lenore D. Zuck (PLAS, 2013)

A Witnessing Compiler: A Proof of Concept. - Kedar S. Namjoshi; Giacomo Tagliabue; Lenore D. Zuck (RV, 2013)

Witnessing Program Transformations. - Kedar S. Namjoshi; Lenore D. Zuck (SAS, 2013)

Model Check What You Can, Runtime Verify the Rest. - Timothy L. Hinrichs; A. Prasad Sistla; Lenore D. Zuck (HOWARD-60, 2014)

Reasoning about Network Topologies in Space. - Lenore D. Zuck; Kenneth L. McMillan (FPS@ETAPS, 2014)

Ethics in Data Sharing: Developing a Model for Best Practice. - Sven Dietrich; Jeroen van der Ham; Aiko Pras; Roland van Rijswijk-Deij; Darren Shou; Anna Sperotto; Aimee van Wynsberghe; Lenore D. Zuck (IEEE Symposium on Security and Privacy Workshops, 2014)

Limited Mobility, Eventual Stability. - Lenore D. Zuck; Sanjiva Prasad (Haifa Verification Conference, 2015)

A Switch, in Time. - Lenore D. Zuck; Sanjiva Prasad (TGC, 2015)

From Verification to Optimizations. - Rigel Gjomemo; Kedar S. Namjoshi; Phu H. Phung; V. N. Venkatakrishnan; Lenore D. Zuck (VMCAI, 2015)

Runtime verification: the application perspective. - Yliès Falcone; Lenore D. Zuck (Int. J. Softw. Tools Technol. Transf., 2015)

Leveraging Static Analysis Tools for Improving Usability of Memory Error Sanitization Compilers. - Rigel Gjomemo; Phu H. Phung; Edmund Ballou; Kedar S. Namjoshi; V. N. Venkatakrishnan; Lenore D. Zuck (QRS, 2016)

Self-Similarity Breeds Resilience. - Sanjiva Prasad; Lenore D. Zuck (EXPRESS/SOS, 2016)

From Model Checking to a Temporal Proof for Partial Models. - Anna Bernasconi 002; Claudio Menghi; Paola Spoletini; Lenore D. Zuck; Carlo Ghezzi (SEFM, 2017)

From model checking to a temporal proof for partial models: preliminary example. - Anna Bernasconi 002; Claudio Menghi; Paola Spoletini; Lenore D. Zuck; Carlo Ghezzi (CoRR, 2017)

Formal Verification of Optimizing Compilers. - Yiji Zhang; Lenore D. Zuck (ICDCIT, 2018)

P^5 : Planner-less Proofs of Probabilistic Parameterized Protocols. - Lenore D. Zuck; Kenneth L. McMillan; Jordan Torf (VMCAI, 2018)

Invisible Invariants Are Neither. - Lenore D. Zuck; Kenneth L. McMillan (From Reactive Systems to Cyber-Physical Systems, 2019)

Compositional Testing of Internet Protocols. - Kenneth L. McMillan; Lenore D. Zuck (SecDev, 2019)

Formal specification and testing of QUIC. - Kenneth L. McMillan; Lenore D. Zuck (SIGCOMM, 2019)

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

Dynamic relocation in ridesharing via fixpoint construction. - Ian A. Kash; Zhongkai Wen; Lenore D. Zuck (UAI, 2022)

A Formal Analysis of Karn's Algorithm. - Max von Hippel; Kenneth L. McMillan; Cristina Nita-Rotaru; Lenore D. Zuck (NETYS, 2023)

A Case Study in Analytic Protocol Analysis in ACL2. - Max von Hippel; Panagiotis Manolios; Kenneth L. McMillan; Cristina Nita-Rotaru; Lenore D. Zuck (ACL2, 2023)

Avoiding Spurious Timeouts. - Lenore D. Zuck; Zhongkai Wen (Principles of Verification (3), 2024)

Decentralized Fair Division. - Joel Miller; Rishi Advani; Ian A. Kash; Chris Kanich; Lenore D. Zuck (CoRR, 2024)

Program Correctness through Self-Certification. - Kedar S. Namjoshi; Lenore D. Zuck (Commun. ACM, 2025)

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