Publications Since 2000

Validation of Compiler Optimizations

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

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 to appean in Journal of Computer Security

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
(To Appear in a special issue of Computer Languages).

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

Model Checking and Abstraction to the Aid of Parameterized Systems,
L. Zuck and A. Pnueli.
(To appear in Journal of Computer Languages).

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

Invisible Strategies
L. Zuck, Y. Fang, and K. McMillan
Run-Time Results

Model Checking

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