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.)