Photo of Zuck, Lenore

Lenore Zuck

Research Professor

Department of Computer Science

Contact

Building & Room:

1228E SELW

Address:

900 West Taylor Street, MC 152, Chicago, IL, 60607

Office Phone:

(312) 355-1339

Email:

zuck@uic.edu

Related Sites:

About

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)

301

Selected Publications

Translation Validation

Validation of Optimizing Compilers,
L. Zuck, A. Pnueli, and R. Leviahtan.
Weizmann Institute of Science Technical Report MCS01-12, August 2001.

VOC: A Translation Validator for Optimizing Compilers,
L. Zuck, A. Pnueli, Y.Fang, and B. Goldberg.
(COCV’02, 2002.)

VOC: A Methodology for Translation Validation of Optimizing Compilers,
L. Zuck, A. Pnueli, Y.Fang, and B. Goldberg.
(Journal of Universal Computer Science 9(3))

Translation and Run-Time Validation for Optimized Code,
L. Zuck, A. Pnueli, Y.Fang, B. Goldberg, and Y.Hu.
(RV 2002.)

Translation and Run-Time Validation for Optimized Code,
L. Zuck, A. Pnueli, B. Goldberg, C. Barrett, Y.Fang, and Y.Hu.
(To Appear in Journal of Formal Methods in System Design )

Run-Time of Speculative Optimizations using CVC,
C. Barrett, B. Goldberg, and L. Zuck
(RV 2003.)

Into the Loops ,
B. Goldberg, L. Zuck, and C. Barrett
(COCV 2004.)

TVOC: A Translation Validator for Optimizing Compilers ,
C. Barrett, Y. Fang, Y. Hu, B. Goldberg, A. Pnueli, and L. D. Zuck
(CAV 2005.)

Generating Invariants for Translation Validation,
Y. Fand and L. Zuck
(COCV 2006.)

Formal Verification of Backward Compatibility of Microcode
T. Arons, E. Elster, L. Fix, S. Mador-Haim, M. Mishaeli, J. Shalev, E. Singerman, A. Tiemeyer, M. Y. Vardi, and L. D. Zuck, “L. Zuck
(CAV 2005.)

Formal Analysis of Security Protocols

The Faithfulness of Abstract Protocol Analysis: Message Authentication,
J. D. Guttman, J. Thayer, and L.D. Zuck
(ACM CCS-8.) Final version appean in Journal of Computer Security 2004

Parameterized Systems

Automatic Deductive Verification with Invisible Invariants,
A. Pnueli, S. Ruah, and L. Zuck
(TACAS 2001.)

Parameterized Verification with Automatically Computed Inductive Assertions ,
T. Arons, A. Pnueli, S. Ruah, J. Xu, and L. Zuck.
(CAV 2001).

Liveness with (0,1,infinity)-Counter Abstraction,
A. Pnueli, J. Xu, and L. Zuck.
(CAV02).
Run-Time Results

Network Invariants in Action,
Y. Kesten, A. Pnueli, E. Shahar, and L. Zuck.
(CONCUR02).

Model Checking and Abstraction to the Aid of Parameterized Systems,
L. Zuck and A. Pnueli
(Computer Lanugages, Systems, and Structures, 30(3-4). 2004).

Liveness with Invisible Ranking,
Yi Fang, Nir Piterman, A. Pnueli and L. Zuck.
(VMCAI’04).
Run-Time Results

Liveness with Incomprehensible Ranking,
Yi Fang, Nir Piterman, A. Pnueli and L. Zuck.
(TACAS’04).
Run-Time Results

IIV: An Invisible Invariant Verifier,
I.~Balaban, Y.~Fang, A.~Pnueli, and L.~D.~Zuck
(CAV 2005)

Invisible Safety of Distributed Protocols,
I.~Balaban, A.~Pnueli, and L.~D.~Zuck
(ICALP 2006)

Livness by Invisible Invariants,
Y.~Fang, K.~McMillan, A.~Pnueli, and L.~D.~Zuck
(FORTE 2006)

Probabilistic Verification

Automatic Verification of Probabilistic Free Choice
L. Zuck, A. Pnueli, and Yonit Kesten
(VMCAI 2002.)

Automatic Verification by Probabilistic Abstraction
T. Arons, L. Zuck, A. and Pnueli
(FOSSACS 2003.)
Run-Time Results

Monitors

Taming Specifications
T. Margaria, A. P. Sistla, B. Steffen, and L. Zuck,
(CONCUR 2005.)

Monitoring Off-the-Shelf Componenets
P. Sistla, M. Zhou, and L. Zuck,
(VMCAI 2006.)

Monitoring Interfaces for Faults 
Amir Pnueli, Aleksandr Zaks, Lenore Zuck
(ENTCS 2006)

Model Checking/Ranking/Shape Analysis

From Model Checking to a Temporal Proof,
D. Peled and L. Zuck
(SPIN 2001).

From Falsification to Verification,
D. Peled, A. Pnueli, and L. Zuck
(FSTTCS 2001.)

Shape Analysis by Predicate Abstraction,
I. Balaban, A. Pnueli, and L. Zuck
(VMCAI 2005.)

Ranking Abstraction as Companion to Predicate Abstraction,
I. Balaban, A. Pnueli, and L. Zuck
(FORTE 2005.)

Education

Ph.D., Weizmann Institute of Science, 1987