Lenore Zuck

Research Interests:

Theorem proving, formal methods, translation validation, formal analysis of security protocols

Links:

"Beyond Safety" in Schloss Ringberg, April 2004

"Verifying Optimizing Compilers" in Schloss Dagstuhl, July 2005

The Compiler Validation Project

Analysis of Computer SYStems group at NYU

Conferences:

TACAS '05 Tools and Algorithms for the Construction and Analysis of Systems (Edinburgh, April 2005)

TACAS '06 Tools and Algorithms for the Construction and Analysis of Systems (Wienna, April 2006)

TACAS '07 Tools and Algorithms for the Construction and Analysis of Systems (Braga, 2007)

VMCAI '03 Fourth International Conference on Verification, Model Checking, and Abstract Interpretation (NYU, Jan 2003)

VMCAI '04 Fifth International Conference on Verification, Model Checking, and Abstract Interpretation (Venice, Jan 2004)

VMCAI '05 Sixth International Conference on Verification, Model Checking, and Abstract Interpretation (Paris, Jan 2005)

VMCAI '06 Seventh International Conference on Verification, Model Checking, and Abstract Interpretation (Charleston, Jan 2006)

VMCAI '07 Eighth International Conference on Verification, Model Checking, and Abstract Interpretation (Nice, Jan 2007)

CSFW05 18th IEEE Computer Security Foundations Workshop (Aix-en-Provence, June 2005)

CSFW06 19th IEEE Computer Security Foundations Workshop (Venice, June 2006)

CCS05 12th ACM Conference on Computer and Communications Security (Alexandira, VA, Nov 2005)

ATVA05 3rd International Symbopsium on Automated Technology for Verification and Analysis (Oct 2005)

ATVA06 4th International Symbopsium on Automated Technology for Verification and Analysis (Beijing, Oct 2006)

ISoLA '04 International Symposium on Leveraging Applications of Formal Methods (Cyprus, 2004)

COCV '04 Third International Workshop on Compiler Optimization meets Compiler Verification (Barcelona, 2004)

COCV '06 Fifth International Workshop on Compiler Optimization meets Compiler Verification (Wienna, April 2006)

RV03 Third Workshop on Runtime Verification (Boulder, 2003)

RV04 Fourth Workshop on Runtime Verification (Barcelona, 2004)

*Note: Bibliography links coming soon

[1] Nazari Skrupsky, Prithvi Bisht, Timothy Hinrichs, VN Venkatakrishnan, and Lenore Zuck. Tamperproof: a server-agnostic defense for parameter tampering attacks on web applications. In Proceedings of the third ACM conference on Data and application security and privacy, pages 129-140. ACM, 2013. [bib]

[2] Kedar S Namjoshi and Lenore D Zuck. Witnessing program transformations. In Static Analysis, pages 304-323. Springer, 2013. [bib]

[3] Timothy L Hinrichs, Daniele Rossetti, Gabriele Petronella, VN Venkatakrishnan, A Prasad Sistla, and Lenore D Zuck. Weblog: a declarative language for secure web development. In Proceedings of the Eighth ACM SIGPLAN workshop on Programming languages and analysis for security, pages 59-70. ACM, 2013. [bib]

[4] Timothy Hinrichs, Diego Martinoia, William C. Garrison III, Adam Lee, Alessandro Panebianco, and Lenore Zuck. Application-sensitive access control evaluation using parameterized expressiveness. In CSF2013. ACM, 2013. [bib]

[5] Kedar S. Namjohsi, Giacomo Tagliabue, and Lenore D Zuck. A witnessing compiler: A proof of concept. In RV2013, 2013. To Appear. [bib]

[6] Timothy Hinrichs, Michael Cueno, Daniel Ruiz, V. N. Venkatkrishnana, and Lenore D. Zuck. Caveat: Facilitating interactive and secure client-side validators for ruby on rails applications. In SECUREWARE2013, 2013. [bib]

[7] 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. [bib]

[8] José M. Fernandez, Andrew S. Patrick, and Lenore D. Zuck. Ethical and secure data sharing across borders. In Financial Cryptography Workshops, pages 136-140, 2012. [bib]

[9] Matthew L. Bolton, Celeste M. Wallace, and Lenore D. Zuck. On policies and intents. In ICISS, pages 104-118, 2012. [bib]

[10] Yliès Falcone and Lenore D. Zuck. Runtime verification: The application perspective. In ISoLA (1), pages 284-291, 2012. [bib]

[11] Kenneth L. McMillan and Lenore D. Zuck. Invisible invariants and abstract interpretation. In SAS, pages 249-262, 2011. [bib]

[12] Kenneth L McMillan and Lenore D Zuck. Invisible invariants and abstract interpretation. In Static Analysis, pages 249-262. Springer, 2011. [bib]

[13] Ittai Balaban, Amir Pnueli, and Lenore D. Zuck. Proving the refuted: Symbolic model checkers as proof generators. In Concurrency, Compositionality, and Correctness, pages 221-236, 2010. [bib]

[14] Amir Pnueli, Yaniv Sa’ar, and Lenore D. Zuck. JTLV: A framework for developing verification algorithms. In CAV, pages 171-174, 2010. [bib]

[15] Ariel Cohen, Kedar S. Namjoshi, Yaniv Sa’ar, Lenore D. Zuck, and Katya I. Kisyova. Parallelizing a symbolic compositional model-checking algorithm. In Haifa Verification Conference, pages 46-59, 2010. [bib]

[16] Ariel Cohen, Amir Pnueli, and Lenore D Zuck. Mechanical verification of transactional memories with non-transactional memory accesses. In Computer Aided Verification, pages 121-134. Springer, 2008. [bib]

[17] Venkatram Vishwanath, Lenore D Zuck, and Jason Leigh. Specification and verification of lambdaram-a wide-area distributed cache for high performance computing. In Formal Methods and Models for Co-Design, 2008. MEMOCODE 2008. 6th ACM/IEEE International Conference on, pages 187-198. IEEE, 2008. [bib]

[18] 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, 2007. FMCAD’07, pages 37-44. IEEE, 2007. [bib]

[19] Ittai Balaban, Amir Pnueli, and Lenore D Zuck. Shape analysis of single-parent heaps. In Verification, Model Checking, and Abstract Interpretation, pages 91-105. Springer, 2007. [bib]

[20] Ittai Balaban, Amir Pnueli, and Lenore D Zuck. Modular ranking abstraction. International Journal of Foundations of Computer Science, 18(01):5-44, 2007. [bib]

[21] Amir Pnueli, Aleksandr Zaks, and Lenore Zuck. Monitoring interfaces for faults. Electronic Notes in Theoretical Computer Science, 144(4):73-89, 2006. [bib]

[22] 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, pages 356-371. Springer, 2006. [bib]

[23] Ittai Balaban, Amir Pnueli, and Lenore D Zuck. Invisible safety of distributed protocols. In Automata, Languages and Programming, pages 528-539. Springer, 2006. [bib]

[24] Ittai Balaban, Amir Pnueli, and Lenore D Zuck. Shape analysis by predicate abstraction. In Verification, Model Checking, and Abstract Interpretation, pages 164-180. Springer, 2005. [bib]

[25] Clark Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, and Lenore Zuck. Tvoc: A translation validator for optimizing compilers. In Computer Aided Verification, pages 291-295. Springer, 2005. [bib]

[26] Benjamin Goldberg, Lenore Zuck, and Clark Barrett. Into the loops: Practical issues in translation validation for optimizing compilers. Electronic Notes in Theoretical Computer Science, 132(1):53-71, 2005. [bib]

[27] Lenore Zuck, Amir Pnueli, Benjamin Goldberg, Clark Barrett, Yi Fang, and Ying Hu. Translation and run-time validation of loop transformations. Formal Methods in System Design, 27(3):335-360, 2005. [bib]

[28] 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, pages 185-198. Springer, 2005. [bib]

[29] Ittai Balaban, Yi Fang, Amir Pnueli, and Lenore D Zuck. Iiv: An invisible invariant verifier. In Computer Aided Verification, pages 408-412. Springer, 2005. [bib]

[30] 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, pages 1-12. Springer, 2005. [bib]

[31] Tiziana Margaria, A Prasad Sistla, Bernhard Steffen, and Lenore D Zuck. Taming interface specifications. In CONCUR 2005-Concurrency Theory, pages 548-561. Springer, 2005. [bib]

[32] Joshua D Guttman, F Javier Thayer, and Lenore D Zuck. The faithfulness of abstract protocol analysis: Message authentication. Journal of Computer Security, 12(6):865-891, 2004. [bib]

[33] Lenore Zuck and Amir Pnueli. Model checking and abstraction to the aid of parameterized systems (a survey). Computer Languages, Systems & Structures, 30(3):139-169, 2004. [bib]

[34] Yi Fang, Nir Piterman, Amir Pnueli, and Lenore Zuck. Liveness with incomprehensible ranking. In Tools and Algorithms for the Construction and Analysis of Systems, pages 482-496. Springer, 2004. [bib]

[35] Lenore D Zuck, Amir Pnueli, and Benjamin Goldberg. Voc: A methodology for the translation validation of optimizingcompilers. J. UCS, 9(3):223-247, 2003. [bib]

[36] Amir Pnueli and Lenore Zuck. Parameterized verification by probabilistic abstraction. In Foundations of Software Science and Computation Structures, pages 87-102. Springer, 2003. [bib]

[37] Clark Barrett, Benjamin Goldberg, and Lenore Zuck. Run-time validation of speculative optimizations using cvc. Electronic Notes in Theoretical Computer Science, 89(2):89-107, 2003. [bib]

[38] Amir Pnueli, Jessie Xu, and Lenore Zuck. Liveness with (0, 1,∞)-counter abstraction. In Computer Aided Verification, pages 107-122. Springer, 2002. [bib]

[39] Lenore Zuck, Amir Pnueli, Yi Fang, and Benjamin Goldberg. Voc: A translation validator for optimizing compilers1 1this research was supported in part by nsf grant ccr-0098299, onr grant n00014-99-1-0131, and the minerva center for verification of reactive systems, a gift from intel, a grant from the german-israel foundation for scientific research and development. Electronic notes in theoretical computer science, 65(2):2-18, 2002. [bib]

[40] Yonit Kesten, Amir Pnueli, Elad Shahar, and Lenore Zuck. Network invariants in action. In CONCUR 2002—Concurrency Theory, pages 101-115. Springer, 2002. [bib]

[41] Lenore Zuck, Amir Pnueli, Yi Fang, Benjamin Goldberg, and Ying Hu. Translation and run-time validation of optimized code. Electronic Notes in Theoretical Computer Science, 70(4):179-200, 2002. [bib]

[42] Lenore Zuck, Amir Pnueli, and Yonit Kesten. Automatic verification of probabilistic free choice. In Verification, Model Checking, and Abstract Interpretation, pages 208-224. Springer, 2002. [bib]

[43] Amir Pnueli, Sitvanit Ruah, and Lenore Zuck. Automatic deductive verification with invisible invariants. In Tools and Algorithms for the Construction and Analysis of Systems, pages 82-97. Springer, 2001. [bib]

[44] Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Ying Xu, and Lenore Zuck. Parameterized verification with automatically computed inductive assertions? In Computer Aided Verification, pages 221-234. Springer, 2001. [bib]

[45] Doron Peled, Amir Pnueli, and Lenore Zuck. From falsification to verification. In FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science, pages 292-304. Springer, 2001. [bib]

[46] Doron Peled and Lenore Zuck. From model checking to a temporal proof. In Model Checking Software, pages 1-14. Springer, 2001. [bib]

[47] Lenore Zuck, Amir Pnueli, and Raya Leviathan. Validation of optimizing compilers. In Weizmann Institute of Science. Citeseer, 2001. [bib]

[48] David Gelernter and Lenore Zuck. On what linda is: Formal description of linda as a reactive system. In Coordination Languages and Models, pages 187-204. Springer, 1997. [bib]

[49] Nicholas Carriero, David Gelernter, and Lenore Zuck. Bauhaus linda. In Object-based models and languages for concurrent systems, pages 66-76. Springer, 1995. [bib]

[50] Yehuda Afek, Hagit Attiya, Alan Fekete, Michael Fischer, Nancy Lynch, Yishay Mansour, Dai-Wei Wang, and Lenore Zuck. Reliable communication over unreliable channels. Journal of the ACM (JACM), 41(6):1267-1297, 1994. [bib]

[51] Amir Pnueli and Lenore D Zuck. Probabilistic verification. Information and computation, 103(1):1-29, 1993. [bib]

[52] A Prasad Sistla and Lenore D Zuck. Reasoning in a restricted temporal logic. Information and Computation, 102(2):167-195, 1993. [bib]

[53] A Pnueli and Lenore Zuck. In and out of temporal logic. In Logic in Computer Science, 1993. LICS’93., Proceedings of Eighth Annual IEEE Symposium on, pages 124-135. IEEE, 1993. [bib]

[54] 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. Journal of the ACM (JACM), 39(3):449-478, 1992. [bib]

[55] Henri B Weinberg and Lenore D Zuck. Timed ethernet: Real-time formal specification of ethernet. In CONCUR’92, pages 370-385. Springer, 1992. [bib]

[56] A Prasad Sistla and Lenore D Zuck. Automatic temporal verification of buffer systems. In Computer Aided Verification, pages 59-69. Springer, 1992. [bib]

[57] Nick Reingold, Da-Wei Wang, and Lenore D Zuck. Games i/o automata play. In CONCUR’92, pages 325-339. Springer, 1992. [bib]

[58] Da-Wei Wang and Lenore Zuck. Real-time sequence transmission problem. In Proceedings of the tenth annual ACM symposium on Principles of distributed computing, pages 111-123. ACM, 1991. [bib]

[59] 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, pages 73-83. ACM, 1989. [bib]

[60] 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, pages 142-158. Springer, 1988. [bib]

[61] Lenore Zuck. Past temporal logic. Ann Arbor, 1001:48106-1346, 1987. [bib]

[62] A Prasad Sistla and Lenore D Zuck. On the eventuality operator in temporal logic. In LICS, pages 153-166, 1987. [ bib ]

[63] Amir Pnueli and Lenore Zuck. Verification of multiprocess probabilistic protocols. Distributed Computing, 1(1):53-72, 1986. [bib]

[64] Amir Pnueli and Lenore D Zuck. Probabilistic verification by tableaux. In LICS, pages 322-331, 1986. [bib]

[65] Orna Lichtenstein, Amir Pnueli, and Lenore Zuck. The glory of the past. Springer, 1985. [bib]

Ph.D., Weizmann Institute of Science, 1987