Lenore D. Zuck

107 papers A* 17A 5B 20C 5Misc 2Journal 22Unranked 35

Year	Rank	Type	Title / Venue / Authors
2026	—	`conf`	Liveness to Safety for Distributed Systems. On the Pursuit of Insight and Elegance Lenore D. Zuck
2025	J	`jnl`	It Takes a Village: Bridging the Gaps between Current and Formal Specifications for Protocols. Commun. ACM David A. Basin, Nate Foster, Kenneth L. McMillan, Kedar S. Namjoshi, Cristina Nita-Rotaru, Jonathan M. Smith, Pamela Zave, Lenore D. Zuck
2025	J	`jnl`	It Takes a Village: Bridging the Gaps between Current and Formal Specifications for Protocols. CoRR David A. Basin, Nate Foster, Kenneth L. McMillan, Kedar S. Namjoshi, Cristina Nita-Rotaru, Jonathan M. Smith, Pamela Zave, Lenore D. Zuck
2025	J	`jnl`	Program Correctness through Self-Certification. Commun. ACM Kedar S. Namjoshi, Lenore D. Zuck
2024	—	`conf`	Avoiding Spurious Timeouts. Principles of Verification (3) Lenore D. Zuck, Zhongkai Wen
2024	J	`jnl`	Decentralized Fair Division. CoRR Joel Miller, Rishi Advani, Ian A. Kash, Chris Kanich, Lenore D. Zuck
2023	—	`conf`	A Case Study in Analytic Protocol Analysis in ACL2. ACL2 Max von Hippel, Panagiotis Manolios, Kenneth L. McMillan, Cristina Nita-Rotaru, Lenore D. Zuck
2023	—	`conf`	A Formal Analysis of Karn's Algorithm. NETYS Max von Hippel, Kenneth L. McMillan, Cristina Nita-Rotaru, Lenore D. Zuck
2022	A	`conf`	Dynamic relocation in ridesharing via fixpoint construction. UAI Ian A. Kash, Zhongkai Wen, Lenore D. Zuck
2020	J	`jnl`	Assured Autonomy: Path Toward Living With Autonomous Systems We Can Trust. CoRR Ufuk Topcu, Nadya Bliss, Nancy J. Cooke, Missy L. Cummings, Ashley J. Llorens, Howard E. Shrobe, Lenore D. Zuck
2019	—	`conf`	Compositional Testing of Internet Protocols. SecDev Kenneth L. McMillan, Lenore D. Zuck
2019	A*	`conf`	Formal specification and testing of QUIC. SIGCOMM Kenneth L. McMillan, Lenore D. Zuck
2019	—	`conf`	Invisible Invariants Are Neither. From Reactive Systems to Cyber-Physical Systems Lenore D. Zuck, Kenneth L. McMillan
2018	Misc	`conf`	Formal Verification of Optimizing Compilers. ICDCIT Yiji Zhang, Lenore D. Zuck
2018	B	`conf`	P^5 : Planner-less Proofs of Probabilistic Parameterized Protocols. VMCAI Lenore D. Zuck, Kenneth L. McMillan, Jordan Torf
2017	B	`conf`	From Model Checking to a Temporal Proof for Partial Models. SEFM Anna Bernasconi, Claudio Menghi, Paola Spoletini, Lenore D. Zuck, Carlo Ghezzi
2017	J	`jnl`	From model checking to a temporal proof for partial models: preliminary example. CoRR Anna Bernasconi, Claudio Menghi, Paola Spoletini, Lenore D. Zuck, Carlo Ghezzi
2016	C	`conf`	Leveraging Static Analysis Tools for Improving Usability of Memory Error Sanitization Compilers. QRS Rigel Gjomemo, Phu H. Phung, Edmund Ballou, Kedar S. Namjoshi, V. N. Venkatakrishnan, Lenore D. Zuck
2016	—	`conf`	Self-Similarity Breeds Resilience. EXPRESS/SOS Sanjiva Prasad, Lenore D. Zuck
2015	—	`conf`	A Switch, in Time. TGC Lenore D. Zuck, Sanjiva Prasad
2015	B	`conf`	From Verification to Optimizations. VMCAI Rigel Gjomemo, Kedar S. Namjoshi, Phu H. Phung, V. N. Venkatakrishnan, Lenore D. Zuck
2015	—	`conf`	Limited Mobility, Eventual Stability. Haifa Verification Conference Lenore D. Zuck, Sanjiva Prasad
2015	J	`jnl`	Runtime verification: the application perspective. Int. J. Softw. Tools Technol. Transf. Yliès Falcone, Lenore D. Zuck
2014	—	`conf`	Ethics in Data Sharing: Developing a Model for Best Practice. IEEE Symposium on Security and Privacy Workshops Sven Dietrich, Jeroen van der Ham, Aiko Pras, Roland van Rijswijk-Deij, Darren Shou, Anna Sperotto, Aimee van Wynsberghe, Lenore D. Zuck
2014	—	`ch.`	Model Check What You Can, Runtime Verify the Rest. HOWARD-60 Timothy L. Hinrichs, A. Prasad Sistla, Lenore D. Zuck
2014	—	`conf`	Reasoning about Network Topologies in Space. FPS@ETAPS Lenore D. Zuck, Kenneth L. McMillan
2013	B	`conf`	A Witnessing Compiler: A Proof of Concept. RV Kedar S. Namjoshi, Giacomo Tagliabue, Lenore D. Zuck
2013	A	`conf`	Application-Sensitive Access Control Evaluation Using Parameterized Expressiveness. CSF Timothy L. Hinrichs, Diego Martinoia, William C. Garrison III, Adam J. Lee, Alessandro Panebianco, Lenore D. Zuck
2013	—	`conf`	TamperProof: a server-agnostic defense for parameter tampering attacks on web applications. CODASPY Nazari Skrupsky, Prithvi Bisht, Timothy L. Hinrichs, V. N. Venkatakrishnan, Lenore D. Zuck
2013	—	`conf`	WEBLOG: a declarative language for secure web development. PLAS Timothy L. Hinrichs, Daniele Rossetti, Gabriele Petronella, V. N. Venkatakrishnan, A. Prasad Sistla, Lenore D. Zuck
2013	B	`conf`	Witnessing Program Transformations. SAS Kedar S. Namjoshi, Lenore D. Zuck
2012	—	`conf`	Don't Repeat Yourself: Automatically Synthesizing Client-side Validation Code for Web Applications. WebApps Nazari Skrupsky, Maliheh Monshizadeh, Prithvi Bisht, Timothy L. Hinrichs, Venkat N. Venkatakrishnan, Lenore D. Zuck
2012	J	`jnl`	Editorʼs foreword. J. Comput. Syst. Sci. Ahmed Bouajjani, David Harel, Lenore D. Zuck
2012	—	`conf`	Ethical and Secure Data Sharing across Borders. Financial Cryptography Workshops José M. Fernandez, Andrew S. Patrick, Lenore D. Zuck
2012	Misc	`conf`	On Policies and Intents. ICISS Matthew L. Bolton, Celeste M. Wallace, Lenore D. Zuck
2012	—	`conf`	Runtime Verification: The Application Perspective. ISoLA (1) Yliès Falcone, Lenore D. Zuck
2012	J	`jnl`	Verification of multi-linked heaps. J. Comput. Syst. Sci. Ittai Balaban, Amir Pnueli, Yaniv Sa'ar, Lenore D. Zuck
2012	—	`conf`	WAVES: Automatic Synthesis of Client-Side Validation Code for Web Applications. CyberSecurity Nazari Skrupsky, Maliheh Monshizadeh, Prithvi Bisht, Timothy L. Hinrichs, V. N. Venkatakrishnan, Lenore D. Zuck
2011	B	`conf`	Invisible Invariants and Abstract Interpretation. SAS Kenneth L. McMillan, Lenore D. Zuck
2010	A*	`conf`	Jtlv: A Framework for Developing Verification Algorithms. CAV Amir Pnueli, Yaniv Sa'ar, Lenore D. Zuck
2010	—	`conf`	Parallelizing a Symbolic Compositional Model-Checking Algorithm. Haifa Verification Conference Ariel Cohen, Kedar S. Namjoshi, Yaniv Sa'ar, Lenore D. Zuck, Katya I. Kisyova
2010	—	`conf`	Proving the Refuted: Symbolic Model Checkers as Proof Generators. Concurrency, Compositionality, and Correctness Ittai Balaban, Amir Pnueli, Lenore D. Zuck
2009	—	`conf`	Abstract Counterexamples for Non-disjunctive Abstractions. RP Kenneth L. McMillan, Lenore D. Zuck
2008	—	`conf`	Access Control and Information Flow in Transactional Memory. Formal Aspects in Security and Trust Ariel Cohen, Ron van der Meyden, Lenore D. Zuck
2008	A*	`conf`	Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses. CAV Ariel Cohen, Amir Pnueli, Lenore D. Zuck
2008	C	`conf`	Specification and Verification of LambdaRAM: A Wide-area Distributed Cache for High Performance Computing. MEMOCODE Venkatram Vishwanath, Lenore D. Zuck, Jason Leigh
2008	B	`ed.`	Verification, Model Checking, and Abstract Interpretation, 9th International Conference, VMCAI 2008, San Francisco, USA, January 7-9, 2008, Proceedings VMCAI Francesco Logozzo, Doron A. Peled, Lenore D. Zuck
2007	J	`jnl`	Modular Ranking Abstraction. Int. J. Found. Comput. Sci. Ittai Balaban, Amir Pnueli, Lenore D. Zuck
2007	B	`conf`	Shape Analysis of Single-Parent Heaps. VMCAI Ittai Balaban, Amir Pnueli, Lenore D. Zuck
2007	—	`conf`	Test Case Generation for Ultimately Periodic Paths. Haifa Verification Conference Saddek Bensalem, Doron A. Peled, Hongyang Qu, Stavros Tripakis, Lenore D. Zuck
2007	B	`conf`	Verifying Correctness of Transactional Memories. FMCAD Ariel Cohen, John W. O'Leary, Amir Pnueli, Mark R. Tuttle, Lenore D. Zuck
2006	—	`conf`	Improved Invariant Generation for Tvoc. COCV Yi Fang, Lenore D. Zuck
2006	—	`conf`	Invisible Safety of Distributed Protocols. ICALP (2) Ittai Balaban, Amir Pnueli, Lenore D. Zuck
2006	C	`conf`	Liveness by Invisible Invariants. FORTE Yi Fang, Kenneth L. McMillan, Amir Pnueli, Lenore D. Zuck
2006	J	`jnl`	Liveness with invisible ranking. Int. J. Softw. Tools Technol. Transf. Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck
2006	B	`conf`	Monitoring Off-the-Shelf Components. VMCAI A. Prasad Sistla, Min Zhou, Lenore D. Zuck
2005	A*	`conf`	Formal Verification of Backward Compatibility of Microcode. CAV Tamarah Arons, Elad Elster, Limor Fix, Sela Mador-Haim, Michael Mishaeli, Jonathan Shalev, Eli Singerman, Andreas Tiemeyer, Moshe Y. Vardi, Lenore D. Zuck
2005	—	`conf`	From Requirements to Specifications. ECBS Cory Plock, Benjamin Goldberg, Lenore D. Zuck
2005	A*	`conf`	IIV: An Invisible Invariant Verifier. CAV Ittai Balaban, Yi Fang, Amir Pnueli, Lenore D. Zuck
2005	—	`conf`	Monitoring Interfaces for Faults. RV@CAV Amir Pnueli, Aleksandr Zaks, Lenore D. Zuck
2005	C	`conf`	Ranking Abstraction as Companion to Predicate Abstraction. FORTE Ittai Balaban, Amir Pnueli, Lenore D. Zuck
2005	B	`conf`	Shape Analysis by Predicate Abstraction. VMCAI Ittai Balaban, Amir Pnueli, Lenore D. Zuck
2005	A*	`conf`	TVOC: A Translation Validator for Optimizing Compilers. CAV Clark W. Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, Lenore D. Zuck
2005	B	`conf`	Taming Interface Specifications. CONCUR Tiziana Margaria, A. Prasad Sistla, Bernhard Steffen, Lenore D. Zuck
2005	A	`ed.`	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 TACAS Nicolas Halbwachs, Lenore D. Zuck
2005	J	`jnl`	Translation and Run-Time Validation of Loop Transformations. Formal Methods Syst. Des. Lenore D. Zuck, Amir Pnueli, Benjamin Goldberg, Clark W. Barrett, Yi Fang, Ying Hu
2004	—	`conf`	Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers. COCV Benjamin Goldberg, Lenore D. Zuck, Clark W. Barrett
2004	A	`conf`	Liveness with Incomprehensible Ranking. TACAS Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck
2004	B	`conf`	Liveness with Invisible Ranking. VMCAI Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck
2004	J	`jnl`	Model checking and abstraction to the aid of parameterized systems (a survey). Comput. Lang. Syst. Struct. Lenore D. Zuck, Amir Pnueli
2004	J	`jnl`	Preface by the section editors. Int. J. Softw. Tools Technol. Transf. Lenore D. Zuck, Paul C. Attie, Agostino Cortesi
2004	J	`jnl`	Special issue of VMCAI'03. Comput. Lang. Syst. Struct. Lenore D. Zuck
2004	J	`jnl`	The faithfulness of abstract protocol analysis: Message authentication. J. Comput. Secur. Joshua D. Guttman, F. Javier Thayer, Lenore D. Zuck
2003	B	`conf`	Model-Checking and Abstraction to the Aid of Parameterized Systems. VMCAI Amir Pnueli, Lenore D. Zuck
2003	B	`conf`	Parameterized Verification by Probabilistic Abstraction. FoSSaCS Tamarah Arons, Amir Pnueli, Lenore D. Zuck
2003	—	`conf`	Run-Time Validation of Speculative Optimizations using CVC. RV@CAV Clark W. Barrett, Benjamin Goldberg, Lenore D. Zuck
2003	J	`jnl`	VOC: A Methodology for the Translation Validation of OptimizingCompilers. J. Univers. Comput. Sci. Lenore D. Zuck, Amir Pnueli, Benjamin Goldberg
2003	B	`ed.`	Verification, Model Checking, and Abstract Interpretation, 4th International Conference, VMCAI 2003, New York, NY, USA, January 9-11, 2002, Proceedings VMCAI Lenore D. Zuck, Paul C. Attie, Agostino Cortesi, Supratik Mukhopadhyay
2002	B	`conf`	Automatic Verification of Probabilistic Free Choice. VMCAI Lenore D. Zuck, Amir Pnueli, Yonit Kesten
2002	A*	`conf`	Liveness with (0, 1, infty)-Counter Abstraction. CAV Amir Pnueli, Jessie Xu, Lenore D. Zuck
2002	B	`conf`	Network Invariants in Action. CONCUR Yonit Kesten, Amir Pnueli, Elad Shahar, Lenore D. Zuck
2002	—	`conf`	Translation and Run-Time Validation of Optimized Code. RV@FLoC Lenore D. Zuck, Amir Pnueli, Yi Fang, Benjamin Goldberg, Ying Hu
2002	—	`conf`	VOC: A Translation Validator for Optimizing Compilers. COCV Lenore D. Zuck, Amir Pnueli, Yi Fang, Benjamin Goldberg
2001	A	`conf`	Automatic Deductive Verification with Invisible Invariants. TACAS Amir Pnueli, Sitvanit Ruah, Lenore D. Zuck
2001	—	`conf`	From Falsification to Verification. FSTTCS Doron A. Peled, Amir Pnueli, Lenore D. Zuck
2001	—	`conf`	From Model Checking to a Temporal Proof. SPIN Doron A. Peled, Lenore D. Zuck
2001	A*	`conf`	Parameterized Verification with Automatically Computed Inductive Assertions. CAV Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Jiazhao Xu, Lenore D. Zuck
2001	A*	`conf`	The faithfulness of abstract protocol analysis: message authentication. CCS Joshua D. Guttman, F. Javier Thayer, Lenore D. Zuck
1997	C	`conf`	On What Linda Is: Formal Description of Linda as a Reactive System. COORDINATION David Gelernter, Lenore D. Zuck
1994	A*	`conf`	Adaptive Algorithms for PASO Systems. PODC Jeffery R. Westbrook, Lenore D. Zuck
1994	—	`conf`	Bauhaus Linda. ECOOP Workshop Nicholas Carriero, David Gelernter, Lenore D. Zuck
1994	J	`jnl`	Reliable Communication Over Unreliable Channels. J. ACM Yehuda Afek, Hagit Attiya, Alan D. Fekete, Michael J. Fischer, Nancy A. Lynch, Yishay Mansour, Da-Wei Wang, Lenore D. Zuck
1993	A*	`conf`	In and Out of Temporal Logic LICS Amir Pnueli, Lenore D. Zuck
1993	J	`jnl`	Probabilistic Verification Inf. Comput. Amir Pnueli, Lenore D. Zuck
1993	J	`jnl`	Reasoning in a Restricted Temporal Logic Inf. Comput. A. Prasad Sistla, Lenore D. Zuck
1992	J	`jnl`	A Little Knowledge Goes a Long Way: Knowledge-Based Derivations and Correctness Proofs for a Family of Protocols. J. ACM Joseph Y. Halpern, Lenore D. Zuck
1992	B	`conf`	Games I/O Automata Play (Extended Abstract). CONCUR Nick Reingold, Da-Wei Wang, Lenore D. Zuck
1992	B	`conf`	Timed Ethernet: Real-Time Formal Specification of Ethernet. CONCUR Henri B. Weinberg, Lenore D. Zuck
1991	A*	`conf`	Automatic Temporal Verification of Buffer Systems. CAV A. Prasad Sistla, Lenore D. Zuck
1991	A*	`conf`	Real-Time Sequence Transmission Problem. PODC Da-Wei Wang, Lenore D. Zuck
1989	A*	`conf`	Tight Bounds for the Sequence Transmission Problem. PODC Da-Wei Wang, Lenore D. Zuck
1988	—	`conf`	Reasoning about Uncertainty in Fault-tolerant Distributed Systems. FTRTFT Michael J. Fischer, Lenore D. Zuck
1987	A*	`conf`	On the Eventuality Operator in Temporal Logic LICS A. Prasad Sistla, Lenore D. Zuck
1986	A*	`conf`	Probabilistic Verification by Tableaux LICS Amir Pnueli, Lenore D. Zuck
1986	J	`jnl`	Verification of Multiprocess Probabilistic Protocols. Distributed Comput. Amir Pnueli, Lenore D. Zuck
1985	—	`conf`	The Glory of the Past. Logic of Programs Orna Lichtenstein, Amir Pnueli, Lenore D. Zuck
1984	A*	`conf`	Verification of Multiprocess Probabilistic Protocols. PODC Amir Pnueli, Lenore D. Zuck